Module mathcomp.algebra.numeric_hierarchy.numdomain
From HB Require Import structures.From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop finset fingroup nmodule order.
From mathcomp Require Import interval rings_modules_and_algebras divalg poly.
From mathcomp Require Import orderedzmod.
Number structures (numdomain.v)
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
NB: The header of ssrnum.v explains how to use the files in this directory.
This file defines the following number structures:
semiNormedZmodType == Zmodule with a semi-norm
The HB class is called SemiNormedZmodule.
normedZmodType == Zmodule with a norm
The HB class is called NormedZmodule.
subNormedZmodType S == join of normedZmodType M and subType (S : pred M)
such that val preserves the norm
The HB class is called SubNormedZmodule.
numDomainType == Integral domain with an order and a norm
The HB class is called NumDomain.
realDomainType == Num domain where all elements are positive or
negative
The HB class is called RealDomain.
Over these structures, we have the following operations:
`|x| == norm of x
Num.sg x == sign of x: equal to 0 iff x = 0, to 1 iff x > 0, and
to -1 in all other cases (including x < 0)
- list of prefixes :
p : positive
n : negative
sp : strictly positive
sn : strictly negative
i : interior = in [0, 1] or ]0, 1[
e : exterior = in [1, +oo[ or ]1; +oo[
w : non strict (weak) monotony
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory.
Import orderedzmod.Num.
Module Num.
HB.mixin Record Zmodule_isSemiNormed (R : POrderZmodule.type) M
& GRing.Zmodule M := {
norm : M -> R;
ler_normD : forall x y, norm (x + y) <= norm x + norm y;
normrMn : forall x n, norm (x *+ n) = norm x *+ n;
normrN : forall x, norm (- x) = norm x;
}.
#[short(type="semiNormedZmodType")]
HB.structure Definition SemiNormedZmodule (R : porderZmodType) :=
{ M of Zmodule_isSemiNormed R M & GRing.Zmodule M }.
HB.mixin Record SemiNormedZmodule_isPositiveDefinite
(R : POrderZmodule.type) M & @SemiNormedZmodule R M := {
normr0_eq0 : forall x : M, norm x = 0 -> x = 0;
}.
#[short(type="normedZmodType")]
HB.structure Definition NormedZmodule (R : porderZmodType) :=
{ M of SemiNormedZmodule_isPositiveDefinite R M & SemiNormedZmodule R M }.
Arguments norm {R M} x : rename.
HB.mixin Record Zmodule_isSubNormed (R : porderZmodType) (M : normedZmodType R)
(S : pred M) U & SubType M S U & NormedZmodule R U := {
norm_valE : forall x : U, norm ((val : U -> M) x) = norm x
}.
#[short(type="subNormedZmodType")]
HB.structure Definition SubNormedZmodule (R : porderZmodType)
(M : normedZmodType R) (S : pred M) :=
{ U of SubChoice M S U & Num.NormedZmodule R U & GRing.SubZmodule M S U
& Zmodule_isSubNormed R M S U }.
HB.factory Record Zmodule_isNormed (R : porderZmodType) M
& GRing.Zmodule M := {
norm : M -> R;
ler_normD : forall x y, norm (x + y) <= norm x + norm y;
normr0_eq0 : forall x, norm x = 0 -> x = 0;
normrMn : forall x n, norm (x *+ n) = norm x *+ n;
normrN : forall x, norm (- x) = norm x;
}.
HB.builders Context (R : POrderZmodule.type) M & Zmodule_isNormed R M.
HB.instance Definition _ :=
Zmodule_isSemiNormed.Build R M ler_normD normrMn normrN.
HB.instance Definition _ :=
SemiNormedZmodule_isPositiveDefinite.Build R M normr0_eq0.
HB.end.
Module NormedZmoduleExports.
Bind Scope ring_scope with NormedZmodule.sort.
End NormedZmoduleExports.
HB.export NormedZmoduleExports.
HB.structure Definition POrderSemiNormedZmodule (R : porderZmodType) :=
{ M of POrderZmodule M & Zmodule_isSemiNormed R M}.
HB.structure Definition POrderNormedZmodule (R : porderZmodType) :=
{ M of POrderZmodule M & Zmodule_isNormed R M}.
HB.structure Definition POrderedSemiNormedZmodule (R : porderZmodType) :=
{ M of POrderedZmodule M & Zmodule_isSemiNormed R M}.
HB.structure Definition POrderedNormedZmodule (R : porderZmodType) :=
{ M of POrderedZmodule M & Zmodule_isNormed R M}.
HB.mixin Record NumZmod_isNumRing R & GRing.NzRing R & POrderZmodule R
& NormedZmodule (POrderZmodule.clone R _) R := {
addr_gt0 : forall x y : R, 0 < x -> 0 < y -> 0 < (x + y);
ger_leVge : forall x y : R, 0 <= x -> 0 <= y -> (x <= y) || (y <= x);
normrM : {morph (norm : R -> R) : x y / x * y};
ler_def : forall x y : R, (x <= y) = (norm (y - x) == (y - x));
}.