Library mathcomp.analysis.normedtype
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
Require Import boolp mathcomp_extra ereal reals cardinality.
Require Import classical_sets signed topology prodnormedzmodule.
Require Import functions.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
Require Import boolp mathcomp_extra ereal reals cardinality.
Require Import classical_sets signed topology prodnormedzmodule.
Require Import functions.
This file extends the topological hierarchy with norm-related notions.
Note that balls in topology.v are not necessarily open, here they are.
is_interval E == the set E is an interval
bigcup_ointsub U q == union of open real interval included
in U and that contain the rational
number q
Rhull A == the real interval hull of a set A
shift x y == y + x
center c := shift (- c)
Normed Topological Abelian groups:
pseudoMetricNormedZmodType R == interface type for a normed topological Abelian group equipped with a norm PseudoMetricNormedZmodule.Mixin nb == builds the mixin for a normed topological Abelian group from the compatibility between the norm and balls; the carrier type must have a normed Zmodule over a numDomainType.Normed modules :
normedModType K == interface type for a normed module structure over the numDomainType K. NormedModMixin normZ == builds the mixin for a normed module from the property of the linearity of the norm; the carrier type must have a pseudoMetricNormedZmodType structure NormedModType K T m == packs the mixin m to build a normedModType K; T must have canonical pseudoMetricNormedZmodType K and pseudoMetricType structures. [normedModType K of T for cT] == T-clone of the normedModType K structure cT. [normedModType K of T] == clone of a canonical normedModType K structure on T. `|x| == the norm of x (notation from ssrnum). ball_norm == balls defined by the norm. nbhs_norm == neighborhoods defined by the norm. closed_ball == closure of a ball. f @` [ a , b ], f @` ] a , b [ == notations for images of intervals, intended for continuous, monotonous functions, defined in ring_scope and classical_set_scope respectively as: f @` [ a , b ] := ` [minr (f a) (f b), maxr (f a) (f b) ]%O f @` ] a , b [ := ` ]minr (f a) (f b), maxr (f a) (f b) [%O f @` [ a , b ] := ` [minr (f a) (f b), maxr (f a) (f b) ]%classic f @` ] a , b [ := ` ]minr (f a) (f b), maxr (f a) (f b) [%classicDomination notations:
dominated_by h k f F == `|f| <= k * `|h|, near F bounded_near f F == f is bounded near F [bounded f x | x in A] == f is bounded on A, ie F := globally A [locally [bounded f x | x in A] == f is locally bounded on A bounded_set == set of bounded sets. := [set A | [bounded x | x in A] ] bounded_fun == set of functions bounded on their whole domain. := [set f | [bounded f x | x in setT] ] lipschitz_on f F == f is lipschitz near F [lipschitz f x | x in A] == f is lipschitz on A [locally [lipschitz f x | x in A] == f is locally lipschitz on A k.-lipschitz_on f F == f is k.-lipschitz near F k.-lipschitz_A f == f is k.-lipschitz on A [locally k.-lipschitz_A f] == f is locally k.-lipschitz on AComplete normed modules :
completeNormedModType K == interface type for a complete normed module structure over a realFieldType K. [completeNormedModType K of T] == clone of a canonical complete normed module structure over K on T.Filters :
at_left x, at_right x == filters on real numbers for predicates s.t. nbhs holds on the left/right of x --> We used these definitions to prove the intermediate value theorem and the Heine-Borel theorem, which states that the compact sets of R^n are the closed and bounded sets.Reserved Notation "f @`[ a , b ]" (at level 20, b at level 9,
format "f @`[ a , b ]").
Reserved Notation "f @`] a , b [" (at level 20, b at level 9,
format "f @`] a , b [").
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Definition pointed_of_zmodule (R : zmodType) : pointedType := PointedType R 0.
Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K)
: filteredType R := Filtered.Pack (Filtered.Class
(@Pointed.class (pointed_of_zmodule R))
(nbhs_ball_ (ball_ (fun x ⇒ `|x|)))).
Section pseudoMetric_of_normedDomain.
Variables (K : numDomainType) (R : normedZmodType K).
Lemma ball_norm_center (x : R) (e : K) : 0 < e → ball_ normr x e x.
Lemma ball_norm_symmetric (x y : R) (e : K) :
ball_ normr x e y → ball_ normr y e x.
Lemma ball_norm_triangle (x y z : R) (e1 e2 : K) :
ball_ normr x e1 y → ball_ normr y e2 z → ball_ normr x (e1 + e2) z.
Definition pseudoMetric_of_normedDomain
: PseudoMetric.mixin_of K (@entourage_ K R R (ball_ (fun x ⇒ `|x|)))
:= PseudoMetricMixin ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.
Lemma nbhs_ball_normE :
@nbhs_ball_ K R R (ball_ normr) = nbhs_ (entourage_ (ball_ normr)).
End pseudoMetric_of_normedDomain.
Lemma nbhsN (R : numFieldType) (x : R) :
nbhs (- x) = [set [set - y | y in A] | A in nbhs x].
Lemma openN (R : numFieldType) (A : set R) :
open A → open [set - x | x in A].
Lemma closedN (R : numFieldType) (A : set R) :
closed A → closed [set - x | x in A].
Module PseudoMetricNormedZmodule.
Section ClassDef.
Variable R : numDomainType.
Record mixin_of (T : normedZmodType R) (ent : set (set (T × T)))
(m : PseudoMetric.mixin_of R ent) := Mixin {
_ : PseudoMetric.ball m = ball_ (fun x ⇒ `| x |) }.
Record class_of (T : Type) := Class {
base : Num.NormedZmodule.class_of R T;
pointed_mixin : Pointed.point_of T ;
nbhs_mixin : Filtered.nbhs_of T T ;
topological_mixin : @Topological.mixin_of T nbhs_mixin ;
uniform_mixin : @Uniform.mixin_of T nbhs_mixin ;
pseudoMetric_mixin :
@PseudoMetric.mixin_of R T (Uniform.entourage uniform_mixin) ;
mixin : @mixin_of (Num.NormedZmodule.Pack _ base) _ pseudoMetric_mixin
}.
Definition base2 T c := @PseudoMetric.Class _ _
(@Uniform.Class _
(@Topological.Class _
(Filtered.Class
(Pointed.Class (@base T c) (pointed_mixin c))
(nbhs_mixin c))
(topological_mixin c))
(uniform_mixin c))
(pseudoMetric_mixin c).
TODO: base3?
Structure type (phR : phant R) :=
Pack { sort; _ : class_of sort }.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack (b0 : Num.NormedZmodule.class_of R T) lm0 um0
(m0 : @mixin_of (@Num.NormedZmodule.Pack R (Phant R) T b0) lm0 um0) :=
fun bT (b : Num.NormedZmodule.class_of R T)
& phant_id (@Num.NormedZmodule.class R (Phant R) bT) b ⇒
fun uT (u : PseudoMetric.class_of R T) & phant_id (@PseudoMetric.class R uT) u ⇒
fun (m : @mixin_of (Num.NormedZmodule.Pack _ b) _ u) & phant_id m m0 ⇒
@Pack phR T (@Class T b u u u u u m).
Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition normedZmodType := @Num.NormedZmodule.Pack R phR cT xclass.
Definition pointedType := @Pointed.Pack cT xclass.
Definition filteredType := @Filtered.Pack cT cT xclass.
Definition topologicalType := @Topological.Pack cT xclass.
Definition uniformType := @Uniform.Pack cT xclass.
Definition pseudoMetricType := @PseudoMetric.Pack R cT xclass.
Definition pointed_zmodType := @GRing.Zmodule.Pack pointedType xclass.
Definition filtered_zmodType := @GRing.Zmodule.Pack filteredType xclass.
Definition topological_zmodType := @GRing.Zmodule.Pack topologicalType xclass.
Definition uniform_zmodType := @GRing.Zmodule.Pack uniformType xclass.
Definition pseudoMetric_zmodType := @GRing.Zmodule.Pack pseudoMetricType xclass.
Definition pointed_normedZmodType := @Num.NormedZmodule.Pack R phR pointedType xclass.
Definition filtered_normedZmodType := @Num.NormedZmodule.Pack R phR filteredType xclass.
Definition topological_normedZmodType := @Num.NormedZmodule.Pack R phR topologicalType xclass.
Definition uniform_normedZmodType := @Num.NormedZmodule.Pack R phR uniformType xclass.
Definition pseudoMetric_normedZmodType := @Num.NormedZmodule.Pack R phR pseudoMetricType xclass.
End ClassDef.
Definition numDomain_normedDomainType (R : numDomainType) : type (Phant R) :=
Pack (Phant R) (@Class R _ (NumDomain.normed_mixin (NumDomain.class R))).
Module Exports.
Coercion base : class_of >-> Num.NormedZmodule.class_of.
Coercion base2 : class_of >-> PseudoMetric.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion pointedType : type >-> Pointed.type.
Canonical pointedType.
Coercion filteredType : type >-> Filtered.type.
Canonical filteredType.
Coercion topologicalType : type >-> Topological.type.
Canonical topologicalType.
Coercion uniformType : type >-> Uniform.type.
Canonical uniformType.
Coercion pseudoMetricType : type >-> PseudoMetric.type.
Canonical pseudoMetricType.
Canonical pointed_zmodType.
Canonical filtered_zmodType.
Canonical topological_zmodType.
Canonical uniform_zmodType.
Canonical pseudoMetric_zmodType.
Canonical pointed_normedZmodType.
Canonical filtered_normedZmodType.
Canonical topological_normedZmodType.
Canonical uniform_normedZmodType.
Canonical pseudoMetric_normedZmodType.
Notation pseudoMetricNormedZmodType R := (type (Phant R)).
Notation PseudoMetricNormedZmodType R T m :=
(@pack _ (Phant R) T _ _ _ m _ _ idfun _ _ idfun _ idfun).
Notation "[ 'pseudoMetricNormedZmodType' R 'of' T 'for' cT ]" :=
(@clone _ (Phant R) T cT _ idfun)
(at level 0, format "[ 'pseudoMetricNormedZmodType' R 'of' T 'for' cT ]") :
form_scope.
Notation "[ 'pseudoMetricNormedZmodType' R 'of' T ]" :=
(@clone _ (Phant R) T _ _ idfun)
(at level 0, format "[ 'pseudoMetricNormedZmodType' R 'of' T ]") : form_scope.
End Exports.
End PseudoMetricNormedZmodule.
Export PseudoMetricNormedZmodule.Exports.
Section pseudoMetricnormedzmodule_lemmas.
Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}.
Lemma ball_normE : ball_norm = ball.
End pseudoMetricnormedzmodule_lemmas.
neighborhoods
Section Nbhs'.
Context {R : numDomainType} {T : pseudoMetricType R}.
Lemma ex_ball_sig (x : T) (P : set T) :
¬ (∀ eps : {posnum R}, ¬ (ball x eps%:num `<=` ~` P)) →
{d : {posnum R} | ball x d%:num `<=` ~` P}.
Lemma nbhsC (x : T) (P : set T) :
¬ (∀ eps : {posnum R}, ¬ (ball x eps%:num `<=` ~` P)) →
nbhs x (~` P).
Lemma nbhsC_ball (x : T) (P : set T) :
nbhs x (~` P) → {d : {posnum R} | ball x d%:num `<=` ~` P}.
Lemma nbhs_ex (x : T) (P : T → Prop) : nbhs x P →
{d : {posnum R} | ∀ y, ball x d%:num y → P y}.
End Nbhs'.
Lemma coord_continuous {K : numFieldType} m n i j :
continuous (fun M : 'M[K]_(m, n) ⇒ M i j).
Global Instance Proper_dnbhs_numFieldType (R : numFieldType) (x : R) :
ProperFilter x^'.
Global Instance Proper_dnbhs_realType (R : realType) (x : R) :
ProperFilter x^'.
Definition pinfty_nbhs (R : numFieldType) : set (set R) :=
fun P ⇒ ∃ M, M \is Num.real ∧ ∀ x, M < x → P x.
Arguments pinfty_nbhs R : clear implicits.
Definition ninfty_nbhs (R : numFieldType) : set (set R) :=
fun P ⇒ ∃ M, M \is Num.real ∧ ∀ x, x < M → P x.
Arguments ninfty_nbhs R : clear implicits.
Notation "+oo" := (pinfty_nbhs _) : ring_scope.
Notation "-oo" := (ninfty_nbhs _) : ring_scope.
Section infty_nbhs_instances.
Context {R : numFieldType}.
Let R_topologicalType := [topologicalType of R].
Implicit Types r : R.
Global Instance proper_pinfty_nbhs : ProperFilter (pinfty_nbhs R).
Global Instance proper_ninfty_nbhs : ProperFilter (ninfty_nbhs R).
Lemma near_pinfty_div2 (A : set R) :
(\∀ k \near +oo, A k) → (\∀ k \near +oo, A (k / 2)).
Lemma nbhs_pinfty_gt r : r \is Num.real → \∀ x \near +oo, r < x.
Lemma nbhs_pinfty_ge r : r \is Num.real → \∀ x \near +oo, r ≤ x.
Lemma nbhs_ninfty_lt r : r \is Num.real → \∀ x \near -oo, r > x.
Lemma nbhs_ninfty_le r : r \is Num.real → \∀ x \near -oo, r ≥ x.
End infty_nbhs_instances.
#[global] Hint Extern 0 (is_true (0 < _)) ⇒ match goal with
H : ?x \is_near (nbhs +oo) |- _ ⇒
solve[near: x; ∃ 0 ⇒ _/posnumP[x] //] end : core.
Module NormedModule.
Record mixin_of (K : numDomainType)
(V : pseudoMetricNormedZmodType K) (scale : K → V → V) := Mixin {
_ : ∀ (l : K) (x : V), `| scale l x | = `| l | × `| x |;
}.
Section ClassDef.
Variable K : numDomainType.
Record class_of (T : Type) := Class {
base : PseudoMetricNormedZmodule.class_of K T ;
lmodmixin : GRing.Lmodule.mixin_of K (GRing.Zmodule.Pack base) ;
mixin : @mixin_of K (PseudoMetricNormedZmodule.Pack (Phant K) base)
(GRing.Lmodule.scale lmodmixin)
}.
Structure type (phK : phant K) :=
Pack { sort; _ : class_of sort }.
Variables (phK : phant K) (T : Type) (cT : type phK).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phK T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack b0 l0
(m0 : @mixin_of K (@PseudoMetricNormedZmodule.Pack K (Phant K) T b0)
(GRing.Lmodule.scale l0)) :=
fun bT b & phant_id (@PseudoMetricNormedZmodule.class K (Phant K) bT) b ⇒
fun l & phant_id l0 l ⇒
fun m & phant_id m0 m ⇒ Pack phK (@Class T b l m).
Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition normedZmodType := @Num.NormedZmodule.Pack K phK cT xclass.
Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass.
Definition pointedType := @Pointed.Pack cT xclass.
Definition filteredType := @Filtered.Pack cT cT xclass.
Definition topologicalType := @Topological.Pack cT xclass.
Definition uniformType := @Uniform.Pack cT xclass.
Definition pseudoMetricType := @PseudoMetric.Pack K cT xclass.
Definition pseudoMetricNormedZmodType := @PseudoMetricNormedZmodule.Pack K phK cT xclass.
Definition pointed_lmodType := @GRing.Lmodule.Pack K phK pointedType xclass.
Definition filtered_lmodType := @GRing.Lmodule.Pack K phK filteredType xclass.
Definition topological_lmodType := @GRing.Lmodule.Pack K phK topologicalType xclass.
Definition uniform_lmodType := @GRing.Lmodule.Pack K phK uniformType xclass.
Definition pseudoMetric_lmodType := @GRing.Lmodule.Pack K phK pseudoMetricType xclass.
Definition normedZmod_lmodType := @GRing.Lmodule.Pack K phK normedZmodType xclass.
Definition pseudoMetricNormedZmod_lmodType := @GRing.Lmodule.Pack K phK pseudoMetricNormedZmodType xclass.
End ClassDef.
Module Exports.
Coercion base : class_of >-> PseudoMetricNormedZmodule.class_of.
Coercion base2 : class_of >-> GRing.Lmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
Coercion pointedType : type >-> Pointed.type.
Canonical pointedType.
Coercion filteredType : type >-> Filtered.type.
Canonical filteredType.
Coercion topologicalType : type >-> Topological.type.
Canonical topologicalType.
Coercion uniformType : type >-> Uniform.type.
Canonical uniformType.
Coercion pseudoMetricType : type >-> PseudoMetric.type.
Canonical pseudoMetricType.
Coercion pseudoMetricNormedZmodType : type >-> PseudoMetricNormedZmodule.type.
Canonical pseudoMetricNormedZmodType.
Canonical pointed_lmodType.
Canonical filtered_lmodType.
Canonical topological_lmodType.
Canonical uniform_lmodType.
Canonical pseudoMetric_lmodType.
Canonical normedZmod_lmodType.
Canonical pseudoMetricNormedZmod_lmodType.
Notation normedModType K := (type (Phant K)).
Notation NormedModType K T m := (@pack _ (Phant K) T _ _ m _ _ idfun _ idfun _ idfun).
Notation NormedModMixin := Mixin.
Notation "[ 'normedModType' K 'of' T 'for' cT ]" := (@clone _ (Phant K) T cT _ idfun)
(at level 0, format "[ 'normedModType' K 'of' T 'for' cT ]") : form_scope.
Notation "[ 'normedModType' K 'of' T ]" := (@clone _ (Phant K) T _ _ id)
(at level 0, format "[ 'normedModType' K 'of' T ]") : form_scope.
End Exports.
End NormedModule.
Export NormedModule.Exports.
Module regular_topology.
Section regular_topology.
End regular_topology.
Module Exports.
Canonical pseudoMetricNormedZmodType.
Canonical normedModType.
End Exports.
End regular_topology.
Export regular_topology.Exports.
Module numFieldNormedType.
Section realType.
Variable (R : realType).
End realType.
Section rcfType.
Variable (R : rcfType).
End rcfType.
Section archiFieldType.
Variable (R : archiFieldType).
End archiFieldType.
Section realFieldType.
Variable (R : realFieldType).
Definition lmod_latticeType := [latticeType of realField_lmodType].
Definition lmod_distrLatticeType := [distrLatticeType of realField_lmodType].
Definition lmod_orderType := [orderType of realField_lmodType].
Definition lmod_realDomainType := [realDomainType of realField_lmodType].
Definition lalg_latticeType := [latticeType of realField_lalgType].
Definition lalg_distrLatticeType := [distrLatticeType of realField_lalgType].
Definition lalg_orderType := [orderType of realField_lalgType].
Definition lalg_realDomainType := [realDomainType of realField_lalgType].
Definition alg_latticeType := [latticeType of realField_algType].
Definition alg_distrLatticeType := [distrLatticeType of realField_algType].
Definition alg_orderType := [orderType of realField_algType].
Definition alg_realDomainType := [realDomainType of realField_algType].
Definition comAlg_latticeType := [latticeType of realField_comAlgType].
Definition comAlg_distrLatticeType :=
[distrLatticeType of realField_comAlgType].
Definition comAlg_orderType := [orderType of realField_comAlgType].
Definition comAlg_realDomainType := [realDomainType of realField_comAlgType].
Definition unitAlg_latticeType := [latticeType of realField_unitAlgType].
Definition unitAlg_distrLatticeType :=
[distrLatticeType of realField_unitAlgType].
Definition unitAlg_orderType := [orderType of realField_unitAlgType].
Definition unitAlg_realDomainType := [realDomainType of realField_unitAlgType].
Definition comUnitAlg_latticeType := [latticeType of realField_comUnitAlgType].
Definition comUnitAlg_distrLatticeType :=
[distrLatticeType of realField_comUnitAlgType].
Definition comUnitAlg_orderType := [orderType of realField_comUnitAlgType].
Definition comUnitAlg_realDomainType :=
[realDomainType of realField_comUnitAlgType].
Definition vect_latticeType := [latticeType of realField_vectType].
Definition vect_distrLatticeType := [distrLatticeType of realField_vectType].
Definition vect_orderType := [orderType of realField_vectType].
Definition vect_realDomainType := [realDomainType of realField_vectType].
Definition Falg_latticeType := [latticeType of realField_FalgType].
Definition Falg_distrLatticeType := [distrLatticeType of realField_FalgType].
Definition Falg_orderType := [orderType of realField_FalgType].
Definition Falg_realDomainType := [realDomainType of realField_FalgType].
Definition fieldExt_latticeType := [latticeType of realField_fieldExtType].
Definition fieldExt_distrLatticeType :=
[distrLatticeType of realField_fieldExtType].
Definition fieldExt_orderType := [orderType of realField_fieldExtType].
Definition fieldExt_realDomainType :=
[realDomainType of realField_fieldExtType].
Definition pseudoMetricNormedZmod_latticeType :=
[latticeType of realField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_distrLatticeType :=
[distrLatticeType of realField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_orderType :=
[orderType of realField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_realDomainType :=
[realDomainType of realField_pseudoMetricNormedZmodType].
Definition normedMod_latticeType := [latticeType of realField_normedModType].
Definition normedMod_distrLatticeType :=
[distrLatticeType of realField_normedModType].
Definition normedMod_orderType := [orderType of realField_normedModType].
Definition normedMod_realDomainType :=
[realDomainType of realField_normedModType].
End realFieldType.
Section numClosedFieldType.
Variable (R : numClosedFieldType).
Definition lmod_decFieldType := [decFieldType of numClosedField_lmodType].
Definition lmod_closedFieldType := [closedFieldType of numClosedField_lmodType].
Definition lalg_decFieldType := [decFieldType of numClosedField_lalgType].
Definition lalg_closedFieldType := [closedFieldType of numClosedField_lalgType].
Definition alg_decFieldType := [decFieldType of numClosedField_algType].
Definition alg_closedFieldType := [closedFieldType of numClosedField_algType].
Definition comAlg_decFieldType := [decFieldType of numClosedField_comAlgType].
Definition comAlg_closedFieldType :=
[closedFieldType of numClosedField_comAlgType].
Definition unitAlg_decFieldType := [decFieldType of numClosedField_unitAlgType].
Definition unitAlg_closedFieldType :=
[closedFieldType of numClosedField_unitAlgType].
Definition comUnitAlg_decFieldType :=
[decFieldType of numClosedField_comUnitAlgType].
Definition comUnitAlg_closedFieldType :=
[closedFieldType of numClosedField_comUnitAlgType].
Definition vect_decFieldType := [decFieldType of numClosedField_vectType].
Definition vect_closedFieldType := [closedFieldType of numClosedField_vectType].
Definition Falg_decFieldType := [decFieldType of numClosedField_FalgType].
Definition Falg_closedFieldType := [closedFieldType of numClosedField_FalgType].
Definition fieldExt_decFieldType :=
[decFieldType of numClosedField_fieldExtType].
Definition fieldExt_closedFieldType :=
[closedFieldType of numClosedField_fieldExtType].
Definition pseudoMetricNormedZmod_decFieldType :=
[decFieldType of numClosedField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_closedFieldType :=
[closedFieldType of numClosedField_pseudoMetricNormedZmodType].
Definition normedMod_decFieldType :=
[decFieldType of numClosedField_normedModType].
Definition normedMod_closedFieldType :=
[closedFieldType of numClosedField_normedModType].
End numClosedFieldType.
Section numFieldType.
Variable (R : numFieldType).
Definition lmod_porderType := [porderType of numField_lmodType].
Definition lmod_numDomainType := [numDomainType of numField_lmodType].
Definition lalg_pointedType := [pointedType of numField_lalgType].
Definition lalg_filteredType := [filteredType R of numField_lalgType].
Definition lalg_topologicalType := [topologicalType of numField_lalgType].
Definition lalg_uniformType := [uniformType of numField_lalgType].
Definition lalg_pseudoMetricType := [pseudoMetricType R of numField_lalgType].
Definition lalg_normedZmodType := [normedZmodType R of numField_lalgType].
Definition lalg_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_lalgType].
Definition lalg_normedModType := [normedModType R of numField_lalgType].
Definition lalg_porderType := [porderType of numField_lalgType].
Definition lalg_numDomainType := [numDomainType of numField_lalgType].
Definition alg_pointedType := [pointedType of numField_algType].
Definition alg_filteredType := [filteredType R of numField_algType].
Definition alg_topologicalType := [topologicalType of numField_algType].
Definition alg_uniformType := [uniformType of numField_algType].
Definition alg_pseudoMetricType := [pseudoMetricType R of numField_algType].
Definition alg_normedZmodType := [normedZmodType R of numField_algType].
Definition alg_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_algType].
Definition alg_normedModType := [normedModType R of numField_algType].
Definition alg_porderType := [porderType of numField_algType].
Definition alg_numDomainType := [numDomainType of numField_algType].
Definition comAlg_pointedType := [pointedType of numField_comAlgType].
Definition comAlg_filteredType := [filteredType R of numField_comAlgType].
Definition comAlg_topologicalType := [topologicalType of numField_comAlgType].
Definition comAlg_uniformType := [uniformType of numField_comAlgType].
Definition comAlg_pseudoMetricType :=
[pseudoMetricType R of numField_comAlgType].
Definition comAlg_normedZmodType := [normedZmodType R of numField_comAlgType].
Definition comAlg_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_comAlgType].
Definition comAlg_normedModType := [normedModType R of numField_comAlgType].
Definition comAlg_porderType := [porderType of numField_comAlgType].
Definition comAlg_numDomainType := [numDomainType of numField_comAlgType].
Definition unitAlg_pointedType := [pointedType of numField_unitAlgType].
Definition unitAlg_filteredType := [filteredType R of numField_unitAlgType].
Definition unitAlg_topologicalType := [topologicalType of numField_unitAlgType].
Definition unitAlg_uniformType := [uniformType of numField_unitAlgType].
Definition unitAlg_pseudoMetricType :=
[pseudoMetricType R of numField_unitAlgType].
Definition unitAlg_normedZmodType := [normedZmodType R of numField_unitAlgType].
Definition unitAlg_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_unitAlgType].
Definition unitAlg_normedModType := [normedModType R of numField_unitAlgType].
Definition unitAlg_porderType := [porderType of numField_unitAlgType].
Definition unitAlg_numDomainType := [numDomainType of numField_unitAlgType].
Definition comUnitAlg_pointedType := [pointedType of numField_comUnitAlgType].
Definition comUnitAlg_filteredType :=
[filteredType R of numField_comUnitAlgType].
Definition comUnitAlg_topologicalType :=
[topologicalType of numField_comUnitAlgType].
Definition comUnitAlg_uniformType := [uniformType of numField_comUnitAlgType].
Definition comUnitAlg_pseudoMetricType :=
[pseudoMetricType R of numField_comUnitAlgType].
Definition comUnitAlg_normedZmodType :=
[normedZmodType R of numField_comUnitAlgType].
Definition comUnitAlg_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_comUnitAlgType].
Definition comUnitAlg_normedModType :=
[normedModType R of numField_comUnitAlgType].
Definition comUnitAlg_porderType := [porderType of numField_comUnitAlgType].
Definition comUnitAlg_numDomainType :=
[numDomainType of numField_comUnitAlgType].
Definition vect_pointedType := [pointedType of numField_vectType].
Definition vect_filteredType := [filteredType R of numField_vectType].
Definition vect_topologicalType := [topologicalType of numField_vectType].
Definition vect_uniformType := [uniformType of numField_vectType].
Definition vect_pseudoMetricType := [pseudoMetricType R of numField_vectType].
Definition vect_normedZmodType := [normedZmodType R of numField_vectType].
Definition vect_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_vectType].
Definition vect_normedModType := [normedModType R of numField_vectType].
Definition vect_porderType := [porderType of numField_vectType].
Definition vect_numDomainType := [numDomainType of numField_vectType].
Definition Falg_pointedType := [pointedType of numField_FalgType].
Definition Falg_filteredType := [filteredType R of numField_FalgType].
Definition Falg_topologicalType := [topologicalType of numField_FalgType].
Definition Falg_uniformType := [uniformType of numField_FalgType].
Definition Falg_pseudoMetricType := [pseudoMetricType R of numField_FalgType].
Definition Falg_normedZmodType := [normedZmodType R of numField_FalgType].
Definition Falg_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_FalgType].
Definition Falg_normedModType := [normedModType R of numField_FalgType].
Definition Falg_porderType := [porderType of numField_FalgType].
Definition Falg_numDomainType := [numDomainType of numField_FalgType].
Definition fieldExt_pointedType := [pointedType of numField_fieldExtType].
Definition fieldExt_filteredType := [filteredType R of numField_fieldExtType].
Definition fieldExt_topologicalType :=
[topologicalType of numField_fieldExtType].
Definition fieldExt_uniformType := [uniformType of numField_fieldExtType].
Definition fieldExt_pseudoMetricType :=
[pseudoMetricType R of numField_fieldExtType].
Definition fieldExt_normedZmodType :=
[normedZmodType R of numField_fieldExtType].
Definition fieldExt_pseudoMetricNormedZmodType :=
[pseudoMetricNormedZmodType R of numField_fieldExtType].
Definition fieldExt_normedModType := [normedModType R of numField_fieldExtType].
Definition fieldExt_porderType := [porderType of numField_fieldExtType].
Definition fieldExt_numDomainType := [numDomainType of numField_fieldExtType].
Definition pseudoMetricNormedZmod_ringType :=
[ringType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_comRingType :=
[comRingType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_unitRingType :=
[unitRingType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_comUnitRingType :=
[comUnitRingType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_idomainType :=
[idomainType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_fieldType :=
[fieldType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_porderType :=
[porderType of numField_pseudoMetricNormedZmodType].
Definition pseudoMetricNormedZmod_numDomainType :=
[numDomainType of numField_pseudoMetricNormedZmodType].
Definition normedMod_ringType := [ringType of numField_normedModType].
Definition normedMod_comRingType := [comRingType of numField_normedModType].
Definition normedMod_unitRingType := [unitRingType of numField_normedModType].
Definition normedMod_comUnitRingType :=
[comUnitRingType of numField_normedModType].
Definition normedMod_idomainType := [idomainType of numField_normedModType].
Definition normedMod_fieldType := [fieldType of numField_normedModType].
Definition normedMod_porderType := [porderType of numField_normedModType].
Definition normedMod_numDomainType := [numDomainType of numField_normedModType].
End numFieldType.
Module Exports.
Export topology.numFieldTopology.Exports.
realType
Canonical real_lmodType.
Canonical real_lalgType.
Canonical real_algType.
Canonical real_comAlgType.
Canonical real_unitAlgType.
Canonical real_comUnitAlgType.
Canonical real_vectType.
Canonical real_FalgType.
Canonical real_fieldExtType.
Canonical real_pseudoMetricNormedZmodType.
Canonical real_normedModType.
Coercion real_lmodType : realType >-> lmodType.
Coercion real_lalgType : realType >-> lalgType.
Coercion real_algType : realType >-> algType.
Coercion real_comAlgType : realType >-> comAlgType.
Coercion real_unitAlgType : realType >-> unitAlgType.
Coercion real_comUnitAlgType : realType >-> comUnitAlgType.
Coercion real_vectType : realType >-> vectType.
Coercion real_FalgType : realType >-> FalgType.
Coercion real_fieldExtType : realType >-> fieldExtType.
Coercion real_pseudoMetricNormedZmodType :
realType >-> pseudoMetricNormedZmodType.
Coercion real_normedModType : realType >-> normedModType.
Canonical real_lalgType.
Canonical real_algType.
Canonical real_comAlgType.
Canonical real_unitAlgType.
Canonical real_comUnitAlgType.
Canonical real_vectType.
Canonical real_FalgType.
Canonical real_fieldExtType.
Canonical real_pseudoMetricNormedZmodType.
Canonical real_normedModType.
Coercion real_lmodType : realType >-> lmodType.
Coercion real_lalgType : realType >-> lalgType.
Coercion real_algType : realType >-> algType.
Coercion real_comAlgType : realType >-> comAlgType.
Coercion real_unitAlgType : realType >-> unitAlgType.
Coercion real_comUnitAlgType : realType >-> comUnitAlgType.
Coercion real_vectType : realType >-> vectType.
Coercion real_FalgType : realType >-> FalgType.
Coercion real_fieldExtType : realType >-> fieldExtType.
Coercion real_pseudoMetricNormedZmodType :
realType >-> pseudoMetricNormedZmodType.
Coercion real_normedModType : realType >-> normedModType.
rcfType
Canonical rcf_lmodType.
Canonical rcf_lalgType.
Canonical rcf_algType.
Canonical rcf_comAlgType.
Canonical rcf_unitAlgType.
Canonical rcf_comUnitAlgType.
Canonical rcf_vectType.
Canonical rcf_FalgType.
Canonical rcf_fieldExtType.
Canonical rcf_pseudoMetricNormedZmodType.
Canonical rcf_normedModType.
Coercion rcf_lmodType : rcfType >-> lmodType.
Coercion rcf_lalgType : rcfType >-> lalgType.
Coercion rcf_algType : rcfType >-> algType.
Coercion rcf_comAlgType : rcfType >-> comAlgType.
Coercion rcf_unitAlgType : rcfType >-> unitAlgType.
Coercion rcf_comUnitAlgType : rcfType >-> comUnitAlgType.
Coercion rcf_vectType : rcfType >-> vectType.
Coercion rcf_FalgType : rcfType >-> FalgType.
Coercion rcf_fieldExtType : rcfType >-> fieldExtType.
Coercion rcf_pseudoMetricNormedZmodType :
rcfType >-> pseudoMetricNormedZmodType.
Coercion rcf_normedModType : rcfType >-> normedModType.
Canonical rcf_lalgType.
Canonical rcf_algType.
Canonical rcf_comAlgType.
Canonical rcf_unitAlgType.
Canonical rcf_comUnitAlgType.
Canonical rcf_vectType.
Canonical rcf_FalgType.
Canonical rcf_fieldExtType.
Canonical rcf_pseudoMetricNormedZmodType.
Canonical rcf_normedModType.
Coercion rcf_lmodType : rcfType >-> lmodType.
Coercion rcf_lalgType : rcfType >-> lalgType.
Coercion rcf_algType : rcfType >-> algType.
Coercion rcf_comAlgType : rcfType >-> comAlgType.
Coercion rcf_unitAlgType : rcfType >-> unitAlgType.
Coercion rcf_comUnitAlgType : rcfType >-> comUnitAlgType.
Coercion rcf_vectType : rcfType >-> vectType.
Coercion rcf_FalgType : rcfType >-> FalgType.
Coercion rcf_fieldExtType : rcfType >-> fieldExtType.
Coercion rcf_pseudoMetricNormedZmodType :
rcfType >-> pseudoMetricNormedZmodType.
Coercion rcf_normedModType : rcfType >-> normedModType.
archiFieldType
Canonical archiField_lmodType.
Canonical archiField_lalgType.
Canonical archiField_algType.
Canonical archiField_comAlgType.
Canonical archiField_unitAlgType.
Canonical archiField_comUnitAlgType.
Canonical archiField_vectType.
Canonical archiField_FalgType.
Canonical archiField_fieldExtType.
Canonical archiField_pseudoMetricNormedZmodType.
Canonical archiField_normedModType.
Coercion archiField_lmodType : archiFieldType >-> lmodType.
Coercion archiField_lalgType : archiFieldType >-> lalgType.
Coercion archiField_algType : archiFieldType >-> algType.
Coercion archiField_comAlgType : archiFieldType >-> comAlgType.
Coercion archiField_unitAlgType : archiFieldType >-> unitAlgType.
Coercion archiField_comUnitAlgType : archiFieldType >-> comUnitAlgType.
Coercion archiField_vectType : archiFieldType >-> vectType.
Coercion archiField_FalgType : archiFieldType >-> FalgType.
Coercion archiField_fieldExtType : archiFieldType >-> fieldExtType.
Coercion archiField_pseudoMetricNormedZmodType :
archiFieldType >-> pseudoMetricNormedZmodType.
Coercion archiField_normedModType : archiFieldType >-> normedModType.
Canonical archiField_lalgType.
Canonical archiField_algType.
Canonical archiField_comAlgType.
Canonical archiField_unitAlgType.
Canonical archiField_comUnitAlgType.
Canonical archiField_vectType.
Canonical archiField_FalgType.
Canonical archiField_fieldExtType.
Canonical archiField_pseudoMetricNormedZmodType.
Canonical archiField_normedModType.
Coercion archiField_lmodType : archiFieldType >-> lmodType.
Coercion archiField_lalgType : archiFieldType >-> lalgType.
Coercion archiField_algType : archiFieldType >-> algType.
Coercion archiField_comAlgType : archiFieldType >-> comAlgType.
Coercion archiField_unitAlgType : archiFieldType >-> unitAlgType.
Coercion archiField_comUnitAlgType : archiFieldType >-> comUnitAlgType.
Coercion archiField_vectType : archiFieldType >-> vectType.
Coercion archiField_FalgType : archiFieldType >-> FalgType.
Coercion archiField_fieldExtType : archiFieldType >-> fieldExtType.
Coercion archiField_pseudoMetricNormedZmodType :
archiFieldType >-> pseudoMetricNormedZmodType.
Coercion archiField_normedModType : archiFieldType >-> normedModType.
realFieldType
Canonical realField_lmodType.
Canonical realField_lalgType.
Canonical realField_algType.
Canonical realField_comAlgType.
Canonical realField_unitAlgType.
Canonical realField_comUnitAlgType.
Canonical realField_vectType.
Canonical realField_FalgType.
Canonical realField_fieldExtType.
Canonical realField_pseudoMetricNormedZmodType.
Canonical realField_normedModType.
Canonical lmod_latticeType.
Canonical lmod_distrLatticeType.
Canonical lmod_orderType.
Canonical lmod_realDomainType.
Canonical lalg_latticeType.
Canonical lalg_distrLatticeType.
Canonical lalg_orderType.
Canonical lalg_realDomainType.
Canonical alg_latticeType.
Canonical alg_distrLatticeType.
Canonical alg_orderType.
Canonical alg_realDomainType.
Canonical comAlg_latticeType.
Canonical comAlg_distrLatticeType.
Canonical comAlg_orderType.
Canonical comAlg_realDomainType.
Canonical unitAlg_latticeType.
Canonical unitAlg_distrLatticeType.
Canonical unitAlg_orderType.
Canonical unitAlg_realDomainType.
Canonical comUnitAlg_latticeType.
Canonical comUnitAlg_distrLatticeType.
Canonical comUnitAlg_orderType.
Canonical comUnitAlg_realDomainType.
Canonical vect_latticeType.
Canonical vect_distrLatticeType.
Canonical vect_orderType.
Canonical vect_realDomainType.
Canonical Falg_latticeType.
Canonical Falg_distrLatticeType.
Canonical Falg_orderType.
Canonical Falg_realDomainType.
Canonical fieldExt_latticeType.
Canonical fieldExt_distrLatticeType.
Canonical fieldExt_orderType.
Canonical fieldExt_realDomainType.
Canonical pseudoMetricNormedZmod_latticeType.
Canonical pseudoMetricNormedZmod_distrLatticeType.
Canonical pseudoMetricNormedZmod_orderType.
Canonical pseudoMetricNormedZmod_realDomainType.
Canonical normedMod_latticeType.
Canonical normedMod_distrLatticeType.
Canonical normedMod_orderType.
Canonical normedMod_realDomainType.
Coercion realField_lmodType : realFieldType >-> lmodType.
Coercion realField_lalgType : realFieldType >-> lalgType.
Coercion realField_algType : realFieldType >-> algType.
Coercion realField_comAlgType : realFieldType >-> comAlgType.
Coercion realField_unitAlgType : realFieldType >-> unitAlgType.
Coercion realField_comUnitAlgType : realFieldType >-> comUnitAlgType.
Coercion realField_vectType : realFieldType >-> vectType.
Coercion realField_FalgType : realFieldType >-> FalgType.
Coercion realField_fieldExtType : realFieldType >-> fieldExtType.
Coercion realField_pseudoMetricNormedZmodType :
Num.RealField.type >-> PseudoMetricNormedZmodule.type.
Coercion realField_normedModType : Num.RealField.type >-> NormedModule.type.
Canonical realField_lalgType.
Canonical realField_algType.
Canonical realField_comAlgType.
Canonical realField_unitAlgType.
Canonical realField_comUnitAlgType.
Canonical realField_vectType.
Canonical realField_FalgType.
Canonical realField_fieldExtType.
Canonical realField_pseudoMetricNormedZmodType.
Canonical realField_normedModType.
Canonical lmod_latticeType.
Canonical lmod_distrLatticeType.
Canonical lmod_orderType.
Canonical lmod_realDomainType.
Canonical lalg_latticeType.
Canonical lalg_distrLatticeType.
Canonical lalg_orderType.
Canonical lalg_realDomainType.
Canonical alg_latticeType.
Canonical alg_distrLatticeType.
Canonical alg_orderType.
Canonical alg_realDomainType.
Canonical comAlg_latticeType.
Canonical comAlg_distrLatticeType.
Canonical comAlg_orderType.
Canonical comAlg_realDomainType.
Canonical unitAlg_latticeType.
Canonical unitAlg_distrLatticeType.
Canonical unitAlg_orderType.
Canonical unitAlg_realDomainType.
Canonical comUnitAlg_latticeType.
Canonical comUnitAlg_distrLatticeType.
Canonical comUnitAlg_orderType.
Canonical comUnitAlg_realDomainType.
Canonical vect_latticeType.
Canonical vect_distrLatticeType.
Canonical vect_orderType.
Canonical vect_realDomainType.
Canonical Falg_latticeType.
Canonical Falg_distrLatticeType.
Canonical Falg_orderType.
Canonical Falg_realDomainType.
Canonical fieldExt_latticeType.
Canonical fieldExt_distrLatticeType.
Canonical fieldExt_orderType.
Canonical fieldExt_realDomainType.
Canonical pseudoMetricNormedZmod_latticeType.
Canonical pseudoMetricNormedZmod_distrLatticeType.
Canonical pseudoMetricNormedZmod_orderType.
Canonical pseudoMetricNormedZmod_realDomainType.
Canonical normedMod_latticeType.
Canonical normedMod_distrLatticeType.
Canonical normedMod_orderType.
Canonical normedMod_realDomainType.
Coercion realField_lmodType : realFieldType >-> lmodType.
Coercion realField_lalgType : realFieldType >-> lalgType.
Coercion realField_algType : realFieldType >-> algType.
Coercion realField_comAlgType : realFieldType >-> comAlgType.
Coercion realField_unitAlgType : realFieldType >-> unitAlgType.
Coercion realField_comUnitAlgType : realFieldType >-> comUnitAlgType.
Coercion realField_vectType : realFieldType >-> vectType.
Coercion realField_FalgType : realFieldType >-> FalgType.
Coercion realField_fieldExtType : realFieldType >-> fieldExtType.
Coercion realField_pseudoMetricNormedZmodType :
Num.RealField.type >-> PseudoMetricNormedZmodule.type.
Coercion realField_normedModType : Num.RealField.type >-> NormedModule.type.
numClosedFieldType
Canonical numClosedField_lmodType.
Canonical numClosedField_lalgType.
Canonical numClosedField_algType.
Canonical numClosedField_comAlgType.
Canonical numClosedField_unitAlgType.
Canonical numClosedField_comUnitAlgType.
Canonical numClosedField_vectType.
Canonical numClosedField_FalgType.
Canonical numClosedField_fieldExtType.
Canonical numClosedField_pseudoMetricNormedZmodType.
Canonical numClosedField_normedModType.
Canonical lmod_decFieldType.
Canonical lmod_closedFieldType.
Canonical lalg_decFieldType.
Canonical lalg_closedFieldType.
Canonical alg_decFieldType.
Canonical alg_closedFieldType.
Canonical comAlg_decFieldType.
Canonical comAlg_closedFieldType.
Canonical unitAlg_decFieldType.
Canonical unitAlg_closedFieldType.
Canonical comUnitAlg_decFieldType.
Canonical comUnitAlg_closedFieldType.
Canonical vect_decFieldType.
Canonical vect_closedFieldType.
Canonical Falg_decFieldType.
Canonical Falg_closedFieldType.
Canonical fieldExt_decFieldType.
Canonical fieldExt_closedFieldType.
Canonical pseudoMetricNormedZmod_decFieldType.
Canonical pseudoMetricNormedZmod_closedFieldType.
Canonical normedMod_decFieldType.
Canonical normedMod_closedFieldType.
Coercion numClosedField_lmodType : numClosedFieldType >-> lmodType.
Coercion numClosedField_lalgType : numClosedFieldType >-> lalgType.
Coercion numClosedField_algType : numClosedFieldType >-> algType.
Coercion numClosedField_comAlgType : numClosedFieldType >-> comAlgType.
Coercion numClosedField_unitAlgType : numClosedFieldType >-> unitAlgType.
Coercion numClosedField_comUnitAlgType : numClosedFieldType >-> comUnitAlgType.
Coercion numClosedField_vectType : numClosedFieldType >-> vectType.
Coercion numClosedField_FalgType : numClosedFieldType >-> FalgType.
Coercion numClosedField_fieldExtType : numClosedFieldType >-> fieldExtType.
Coercion numClosedField_pseudoMetricNormedZmodType :
numClosedFieldType >-> pseudoMetricNormedZmodType.
Coercion numClosedField_normedModType : numClosedFieldType >-> normedModType.
Canonical numClosedField_lalgType.
Canonical numClosedField_algType.
Canonical numClosedField_comAlgType.
Canonical numClosedField_unitAlgType.
Canonical numClosedField_comUnitAlgType.
Canonical numClosedField_vectType.
Canonical numClosedField_FalgType.
Canonical numClosedField_fieldExtType.
Canonical numClosedField_pseudoMetricNormedZmodType.
Canonical numClosedField_normedModType.
Canonical lmod_decFieldType.
Canonical lmod_closedFieldType.
Canonical lalg_decFieldType.
Canonical lalg_closedFieldType.
Canonical alg_decFieldType.
Canonical alg_closedFieldType.
Canonical comAlg_decFieldType.
Canonical comAlg_closedFieldType.
Canonical unitAlg_decFieldType.
Canonical unitAlg_closedFieldType.
Canonical comUnitAlg_decFieldType.
Canonical comUnitAlg_closedFieldType.
Canonical vect_decFieldType.
Canonical vect_closedFieldType.
Canonical Falg_decFieldType.
Canonical Falg_closedFieldType.
Canonical fieldExt_decFieldType.
Canonical fieldExt_closedFieldType.
Canonical pseudoMetricNormedZmod_decFieldType.
Canonical pseudoMetricNormedZmod_closedFieldType.
Canonical normedMod_decFieldType.
Canonical normedMod_closedFieldType.
Coercion numClosedField_lmodType : numClosedFieldType >-> lmodType.
Coercion numClosedField_lalgType : numClosedFieldType >-> lalgType.
Coercion numClosedField_algType : numClosedFieldType >-> algType.
Coercion numClosedField_comAlgType : numClosedFieldType >-> comAlgType.
Coercion numClosedField_unitAlgType : numClosedFieldType >-> unitAlgType.
Coercion numClosedField_comUnitAlgType : numClosedFieldType >-> comUnitAlgType.
Coercion numClosedField_vectType : numClosedFieldType >-> vectType.
Coercion numClosedField_FalgType : numClosedFieldType >-> FalgType.
Coercion numClosedField_fieldExtType : numClosedFieldType >-> fieldExtType.
Coercion numClosedField_pseudoMetricNormedZmodType :
numClosedFieldType >-> pseudoMetricNormedZmodType.
Coercion numClosedField_normedModType : numClosedFieldType >-> normedModType.
numFieldType
Canonical numField_lmodType.
Canonical numField_lalgType.
Canonical numField_algType.
Canonical numField_comAlgType.
Canonical numField_unitAlgType.
Canonical numField_comUnitAlgType.
Canonical numField_vectType.
Canonical numField_FalgType.
Canonical numField_fieldExtType.
Canonical numField_pseudoMetricNormedZmodType.
Canonical numField_normedModType.
Canonical lmod_porderType.
Canonical lmod_numDomainType.
Canonical lalg_pointedType.
Canonical lalg_filteredType.
Canonical lalg_topologicalType.
Canonical lalg_uniformType.
Canonical lalg_pseudoMetricType.
Canonical lalg_normedZmodType.
Canonical lalg_pseudoMetricNormedZmodType.
Canonical lalg_normedModType.
Canonical lalg_porderType.
Canonical lalg_numDomainType.
Canonical alg_pointedType.
Canonical alg_filteredType.
Canonical alg_topologicalType.
Canonical alg_uniformType.
Canonical alg_pseudoMetricType.
Canonical alg_normedZmodType.
Canonical alg_pseudoMetricNormedZmodType.
Canonical alg_normedModType.
Canonical alg_porderType.
Canonical alg_numDomainType.
Canonical comAlg_pointedType.
Canonical comAlg_filteredType.
Canonical comAlg_topologicalType.
Canonical comAlg_uniformType.
Canonical comAlg_pseudoMetricType.
Canonical comAlg_normedZmodType.
Canonical comAlg_pseudoMetricNormedZmodType.
Canonical comAlg_normedModType.
Canonical comAlg_porderType.
Canonical comAlg_numDomainType.
Canonical unitAlg_pointedType.
Canonical unitAlg_filteredType.
Canonical unitAlg_topologicalType.
Canonical unitAlg_uniformType.
Canonical unitAlg_pseudoMetricType.
Canonical unitAlg_normedZmodType.
Canonical unitAlg_pseudoMetricNormedZmodType.
Canonical unitAlg_normedModType.
Canonical unitAlg_porderType.
Canonical unitAlg_numDomainType.
Canonical comUnitAlg_pointedType.
Canonical comUnitAlg_filteredType.
Canonical comUnitAlg_topologicalType.
Canonical comUnitAlg_uniformType.
Canonical comUnitAlg_pseudoMetricType.
Canonical comUnitAlg_normedZmodType.
Canonical comUnitAlg_pseudoMetricNormedZmodType.
Canonical comUnitAlg_normedModType.
Canonical comUnitAlg_porderType.
Canonical comUnitAlg_numDomainType.
Canonical vect_pointedType.
Canonical vect_filteredType.
Canonical vect_topologicalType.
Canonical vect_uniformType.
Canonical vect_pseudoMetricType.
Canonical vect_normedZmodType.
Canonical vect_pseudoMetricNormedZmodType.
Canonical vect_normedModType.
Canonical vect_porderType.
Canonical vect_numDomainType.
Canonical Falg_pointedType.
Canonical Falg_filteredType.
Canonical Falg_topologicalType.
Canonical Falg_uniformType.
Canonical Falg_pseudoMetricType.
Canonical Falg_normedZmodType.
Canonical Falg_pseudoMetricNormedZmodType.
Canonical Falg_normedModType.
Canonical Falg_porderType.
Canonical Falg_numDomainType.
Canonical fieldExt_pointedType.
Canonical fieldExt_filteredType.
Canonical fieldExt_topologicalType.
Canonical fieldExt_uniformType.
Canonical fieldExt_pseudoMetricType.
Canonical fieldExt_normedZmodType.
Canonical fieldExt_pseudoMetricNormedZmodType.
Canonical fieldExt_normedModType.
Canonical fieldExt_porderType.
Canonical fieldExt_numDomainType.
Canonical pseudoMetricNormedZmod_ringType.
Canonical pseudoMetricNormedZmod_comRingType.
Canonical pseudoMetricNormedZmod_unitRingType.
Canonical pseudoMetricNormedZmod_comUnitRingType.
Canonical pseudoMetricNormedZmod_idomainType.
Canonical pseudoMetricNormedZmod_fieldType.
Canonical pseudoMetricNormedZmod_porderType.
Canonical pseudoMetricNormedZmod_numDomainType.
Canonical normedMod_ringType.
Canonical normedMod_comRingType.
Canonical normedMod_unitRingType.
Canonical normedMod_comUnitRingType.
Canonical normedMod_idomainType.
Canonical normedMod_fieldType.
Canonical normedMod_porderType.
Canonical normedMod_numDomainType.
Coercion numField_lmodType : numFieldType >-> lmodType.
Coercion numField_lalgType : numFieldType >-> lalgType.
Coercion numField_algType : numFieldType >-> algType.
Coercion numField_comAlgType : numFieldType >-> comAlgType.
Coercion numField_unitAlgType : numFieldType >-> unitAlgType.
Coercion numField_comUnitAlgType : numFieldType >-> comUnitAlgType.
Coercion numField_vectType : numFieldType >-> vectType.
Coercion numField_FalgType : numFieldType >-> FalgType.
Coercion numField_fieldExtType : numFieldType >-> fieldExtType.
Coercion numField_pseudoMetricNormedZmodType :
numFieldType >-> pseudoMetricNormedZmodType.
Coercion numField_normedModType : numFieldType >-> normedModType.
End Exports.
End numFieldNormedType.
Import numFieldNormedType.Exports.
Section NormedModule_numDomainType.
Variables (R : numDomainType) (V : normedModType R).
Lemma normmZ l (x : V) : `| l *: x | = `| l | × `| x |.
End NormedModule_numDomainType.
Section PseudoNormedZmod_numDomainType.
Variables (R : numDomainType) (V : pseudoMetricNormedZmodType R).
Canonical numField_lalgType.
Canonical numField_algType.
Canonical numField_comAlgType.
Canonical numField_unitAlgType.
Canonical numField_comUnitAlgType.
Canonical numField_vectType.
Canonical numField_FalgType.
Canonical numField_fieldExtType.
Canonical numField_pseudoMetricNormedZmodType.
Canonical numField_normedModType.
Canonical lmod_porderType.
Canonical lmod_numDomainType.
Canonical lalg_pointedType.
Canonical lalg_filteredType.
Canonical lalg_topologicalType.
Canonical lalg_uniformType.
Canonical lalg_pseudoMetricType.
Canonical lalg_normedZmodType.
Canonical lalg_pseudoMetricNormedZmodType.
Canonical lalg_normedModType.
Canonical lalg_porderType.
Canonical lalg_numDomainType.
Canonical alg_pointedType.
Canonical alg_filteredType.
Canonical alg_topologicalType.
Canonical alg_uniformType.
Canonical alg_pseudoMetricType.
Canonical alg_normedZmodType.
Canonical alg_pseudoMetricNormedZmodType.
Canonical alg_normedModType.
Canonical alg_porderType.
Canonical alg_numDomainType.
Canonical comAlg_pointedType.
Canonical comAlg_filteredType.
Canonical comAlg_topologicalType.
Canonical comAlg_uniformType.
Canonical comAlg_pseudoMetricType.
Canonical comAlg_normedZmodType.
Canonical comAlg_pseudoMetricNormedZmodType.
Canonical comAlg_normedModType.
Canonical comAlg_porderType.
Canonical comAlg_numDomainType.
Canonical unitAlg_pointedType.
Canonical unitAlg_filteredType.
Canonical unitAlg_topologicalType.
Canonical unitAlg_uniformType.
Canonical unitAlg_pseudoMetricType.
Canonical unitAlg_normedZmodType.
Canonical unitAlg_pseudoMetricNormedZmodType.
Canonical unitAlg_normedModType.
Canonical unitAlg_porderType.
Canonical unitAlg_numDomainType.
Canonical comUnitAlg_pointedType.
Canonical comUnitAlg_filteredType.
Canonical comUnitAlg_topologicalType.
Canonical comUnitAlg_uniformType.
Canonical comUnitAlg_pseudoMetricType.
Canonical comUnitAlg_normedZmodType.
Canonical comUnitAlg_pseudoMetricNormedZmodType.
Canonical comUnitAlg_normedModType.
Canonical comUnitAlg_porderType.
Canonical comUnitAlg_numDomainType.
Canonical vect_pointedType.
Canonical vect_filteredType.
Canonical vect_topologicalType.
Canonical vect_uniformType.
Canonical vect_pseudoMetricType.
Canonical vect_normedZmodType.
Canonical vect_pseudoMetricNormedZmodType.
Canonical vect_normedModType.
Canonical vect_porderType.
Canonical vect_numDomainType.
Canonical Falg_pointedType.
Canonical Falg_filteredType.
Canonical Falg_topologicalType.
Canonical Falg_uniformType.
Canonical Falg_pseudoMetricType.
Canonical Falg_normedZmodType.
Canonical Falg_pseudoMetricNormedZmodType.
Canonical Falg_normedModType.
Canonical Falg_porderType.
Canonical Falg_numDomainType.
Canonical fieldExt_pointedType.
Canonical fieldExt_filteredType.
Canonical fieldExt_topologicalType.
Canonical fieldExt_uniformType.
Canonical fieldExt_pseudoMetricType.
Canonical fieldExt_normedZmodType.
Canonical fieldExt_pseudoMetricNormedZmodType.
Canonical fieldExt_normedModType.
Canonical fieldExt_porderType.
Canonical fieldExt_numDomainType.
Canonical pseudoMetricNormedZmod_ringType.
Canonical pseudoMetricNormedZmod_comRingType.
Canonical pseudoMetricNormedZmod_unitRingType.
Canonical pseudoMetricNormedZmod_comUnitRingType.
Canonical pseudoMetricNormedZmod_idomainType.
Canonical pseudoMetricNormedZmod_fieldType.
Canonical pseudoMetricNormedZmod_porderType.
Canonical pseudoMetricNormedZmod_numDomainType.
Canonical normedMod_ringType.
Canonical normedMod_comRingType.
Canonical normedMod_unitRingType.
Canonical normedMod_comUnitRingType.
Canonical normedMod_idomainType.
Canonical normedMod_fieldType.
Canonical normedMod_porderType.
Canonical normedMod_numDomainType.
Coercion numField_lmodType : numFieldType >-> lmodType.
Coercion numField_lalgType : numFieldType >-> lalgType.
Coercion numField_algType : numFieldType >-> algType.
Coercion numField_comAlgType : numFieldType >-> comAlgType.
Coercion numField_unitAlgType : numFieldType >-> unitAlgType.
Coercion numField_comUnitAlgType : numFieldType >-> comUnitAlgType.
Coercion numField_vectType : numFieldType >-> vectType.
Coercion numField_FalgType : numFieldType >-> FalgType.
Coercion numField_fieldExtType : numFieldType >-> fieldExtType.
Coercion numField_pseudoMetricNormedZmodType :
numFieldType >-> pseudoMetricNormedZmodType.
Coercion numField_normedModType : numFieldType >-> normedModType.
End Exports.
End numFieldNormedType.
Import numFieldNormedType.Exports.
Section NormedModule_numDomainType.
Variables (R : numDomainType) (V : normedModType R).
Lemma normmZ l (x : V) : `| l *: x | = `| l | × `| x |.
End NormedModule_numDomainType.
Section PseudoNormedZmod_numDomainType.
Variables (R : numDomainType) (V : pseudoMetricNormedZmodType R).
if we do not give the V argument to nbhs, the universally quantified set that
appears inside the notation for cvg_to has type
set (let '{| PseudoMetricNormedZmodule.sort := T |} := V in T) instead of set V,
which causes an inference problem in derive.v
Lemma nbhs_le_nbhs_norm (x : V) : @nbhs V _ x `=>` nbhs_norm x.
Lemma nbhs_norm_le_nbhs x : nbhs_norm x `=>` nbhs x.
Lemma nbhs_nbhs_norm : nbhs_norm = nbhs.
Lemma nbhs_normP x P : nbhs x P ↔ nbhs_norm x P.
Lemma filter_from_norm_nbhs x :
@filter_from R _ [set x : R | 0 < x] (ball_norm x) = nbhs x.
Lemma nbhs_normE (x : V) (P : set V) :
nbhs_norm x P = \near x, P x.
Lemma filter_from_normE (x : V) (P : set V) :
@filter_from R _ [set x : R | 0 < x] (ball_norm x) P = \near x, P x.
Lemma near_nbhs_norm (x : V) (P : set V) :
(\∀ x \near nbhs_norm x, P x) = \near x, P x.
Lemma nbhs_norm_ball_norm x (e : {posnum R}) :
nbhs_norm x (ball_norm x e%:num).
Lemma nbhs_ball_norm (x : V) (eps : {posnum R}) : nbhs x (ball_norm x eps%:num).
Lemma ball_norm_dec x y (e : R) : {ball_norm x e y} + {¬ ball_norm x e y}.
Lemma ball_norm_sym x y (e : R) : ball_norm x e y → ball_norm y e x.
Lemma ball_norm_le x (e1 e2 : R) :
e1 ≤ e2 → ball_norm x e1 `<=` ball_norm x e2.
Let nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs).
Lemma cvg_distP {F : set (set V)} {FF : Filter F} (y : V) :
F --> y ↔ ∀ eps, 0 < eps → \∀ y' \near F, `|y - y'| < eps.
Lemma cvg_dist {F : set (set V)} {FF : Filter F} (y : V) :
F --> y → ∀ eps, eps > 0 → \∀ y' \near F, `|y - y'| < eps.
Lemma nbhs_norm_ball x (eps : {posnum R}) : nbhs_norm x (ball x eps%:num).
End PseudoNormedZmod_numDomainType.
#[global] Hint Resolve normr_ge0 : core.
Arguments cvg_dist {_ _ F FF}.
Lemma cvg_gt_ge T (F : set (set T)) (R : realFieldType) {PF : ProperFilter F}
(u : T → R) a b :
u @ F --> b → (a < b)%R → \∀ n \near F, (a ≤ u n)%R.
Lemma cvg_lt_le T (F : set (set T)) (R : realFieldType) {PF : ProperFilter F}
(u : T → R) c b :
u @ F --> b → (b < c)%R → \∀ n \near F, (u n ≤ c)%R.
Lemma pinfty_ex_gt {R : numFieldType} (m : R) (A : set R) : m \is Num.real →
(\∀ k \near +oo, A k) → exists2 M, m < M & A M.
Lemma pinfty_ex_gt0 {R : numFieldType} (A : set R) :
(\∀ k \near +oo, A k) → exists2 M, M > 0 & A M.
Definition self_sub (K : numDomainType) (V W : normedModType K)
(f : V → W) (x : V × V) : W := f x.1 - f x.2.
Arguments self_sub {K V W} f x /.
Definition fun1 {T : Type} {K : numFieldType} : T → K := fun⇒ 1.
Arguments fun1 {T K} x /.
Definition dominated_by {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}
(h : T → V) (k : K) (f : T → W) (F : set (set T)) :=
F [set x | `|f x| ≤ k × `|h x|].
Definition strictly_dominated_by {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}
(h : T → V) (k : K) (f : T → W) (F : set (set T)) :=
F [set x | `|f x| < k × `|h x|].
Lemma sub_dominatedl (T : Type) (K : numFieldType) (V W : pseudoMetricNormedZmodType K)
(h : T → V) (k : K) (F G : set (set T)) : F `=>` G →
(@dominated_by T K V W h k)^~ G `<=` (dominated_by h k)^~ F.
Lemma sub_dominatedr (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
(h : T → V) (k : K) (f g : T → V) (F : set (set T)) (FF : Filter F) :
(\∀ x \near F, `|f x| ≤ `|g x|) →
dominated_by h k g F → dominated_by h k f F.
Lemma dominated_by1 {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
@dominated_by T K _ V fun1 = fun k f F ⇒ F [set x | `|f x| ≤ k].
Lemma strictly_dominated_by1 {T : Type} {K : numFieldType}
{V : pseudoMetricNormedZmodType K} :
@strictly_dominated_by T K _ V fun1 = fun k f F ⇒ F [set x | `|f x| < k].
Lemma ex_dom_bound {T : Type} {K : numFieldType} {V W : pseudoMetricNormedZmodType K}
(h : T → V) (f : T → W) (F : set (set T)) {PF : ProperFilter F}:
(\∀ M \near +oo, dominated_by h M f F) ↔
∃ M, dominated_by h M f F.
Lemma ex_strict_dom_bound {T : Type} {K : numFieldType}
{V W : pseudoMetricNormedZmodType K}
(h : T → V) (f : T → W) (F : set (set T)) {PF : ProperFilter F} :
(\∀ x \near F, h x != 0) →
(\∀ M \near +oo, dominated_by h M f F) ↔
∃ M, strictly_dominated_by h M f F.
Definition bounded_near {T : Type} {K : numFieldType}
{V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) :=
\∀ M \near +oo, F [set x | `|f x| ≤ M].
Lemma boundedE {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
@bounded_near T K V = fun f F ⇒ \∀ M \near +oo, dominated_by fun1 M f F.
Lemma sub_boundedr (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
(F G : set (set T)) : F `=>` G →
(@bounded_near T K V)^~ G `<=` bounded_near^~ F.
Lemma sub_boundedl (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
(f g : T → V) (F : set (set T)) (FF : Filter F) :
(\∀ x \near F, `|f x| ≤ `|g x|) → bounded_near g F → bounded_near f F.
Lemma ex_bound {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) {PF : ProperFilter F}:
bounded_near f F ↔ ∃ M, F [set x | `|f x| ≤ M].
Lemma ex_strict_bound {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) {PF : ProperFilter F}:
bounded_near f F ↔ ∃ M, F [set x | `|f x| < M].
Lemma ex_strict_bound_gt0 {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) {PF : Filter F}:
bounded_near f F → exists2 M, M > 0 & F [set x | `|f x| < M].
Notation "[ 'bounded' E | x 'in' A ]" := (bounded_near (fun x ⇒ E) (globally A))
(at level 0, x name, format "[ 'bounded' E | x 'in' A ]").
Notation bounded_set := [set A | [bounded x | x in A]].
Notation bounded_fun := [set f | [bounded f x | x in setT]].
Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T → R) :
bounded_fun a → has_ubound (range a).
Lemma bounded_funN (T : Type) (R : realFieldType) (a : T → R) :
bounded_fun a → bounded_fun (- a).
Lemma bounded_fun_has_lbound (T : Type) (R : realFieldType) (a : T → R) :
bounded_fun a → has_lbound (range a).
Lemma bounded_funD (T : Type) (R : realFieldType) (a b : T → R) :
bounded_fun a → bounded_fun b → bounded_fun (a \+ b).
Lemma bounded_locally (T : topologicalType)
(R : numFieldType) (V : normedModType R) (A : set T) (f : T → V) :
[bounded f x | x in A] → [locally [bounded f x | x in A]].
Notation "k .-lipschitz_on f" := (dominated_by (self_sub id) k (self_sub f))
(at level 2, format "k .-lipschitz_on f") : type_scope.
Definition sub_klipschitz (K : numFieldType) (V W : normedModType K) (k : K)
(f : V → W) (F G : set (set (V × V))) :
F `=>` G → k.-lipschitz_on f G → k.-lipschitz_on f F.
Definition lipschitz_on (K : numFieldType) (V W : normedModType K)
(f : V → W) (F : set (set (V × V))) :=
\∀ M \near +oo, M.-lipschitz_on f F.
Definition sub_lipschitz (K : numFieldType) (V W : normedModType K)
(f : V → W) (F G : set (set (V × V))) :
F `=>` G → lipschitz_on f G → lipschitz_on f F.
Lemma klipschitzW (K : numFieldType) (V W : normedModType K) (k : K)
(f : V → W) (F : set (set (V × V))) {PF : ProperFilter F} :
k.-lipschitz_on f F → lipschitz_on f F.
Notation "k .-lipschitz_ A f" :=
(k.-lipschitz_on f (globally (A `*` A)))
(at level 2, A at level 0, format "k .-lipschitz_ A f").
Notation "k .-lipschitz f" := (k.-lipschitz_setT f)
(at level 2, format "k .-lipschitz f") : type_scope.
Notation "[ 'lipschitz' E | x 'in' A ]" :=
(lipschitz_on (fun x ⇒ E) (globally (A `*` A)))
(at level 0, x name, format "[ 'lipschitz' E | x 'in' A ]").
Notation lipschitz f := [lipschitz f x | x in setT].
Lemma klipschitz_locally (R : numFieldType) (V W : normedModType R)
(k : R) (f : V → W) (A : set V) :
k.-lipschitz_A f → [locally k.-lipschitz_A f].
Lemma lipschitz_locally (R : numFieldType) (V W : normedModType R)
(A : set V) (f : V → W) :
[lipschitz f x | x in A] → [locally [lipschitz f x | x in A]].
Lemma lipschitz_id (R : numFieldType) (V : normedModType R) : 1.-lipschitz (@id V).
Arguments lipschitz_id {R V}.
Section PseudoNormedZMod_numFieldType.
Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).
Lemma norm_hausdorff : hausdorff_space V.
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: norm_hausdorff] : core.
Lemma nbhs_norm_le_nbhs x : nbhs_norm x `=>` nbhs x.
Lemma nbhs_nbhs_norm : nbhs_norm = nbhs.
Lemma nbhs_normP x P : nbhs x P ↔ nbhs_norm x P.
Lemma filter_from_norm_nbhs x :
@filter_from R _ [set x : R | 0 < x] (ball_norm x) = nbhs x.
Lemma nbhs_normE (x : V) (P : set V) :
nbhs_norm x P = \near x, P x.
Lemma filter_from_normE (x : V) (P : set V) :
@filter_from R _ [set x : R | 0 < x] (ball_norm x) P = \near x, P x.
Lemma near_nbhs_norm (x : V) (P : set V) :
(\∀ x \near nbhs_norm x, P x) = \near x, P x.
Lemma nbhs_norm_ball_norm x (e : {posnum R}) :
nbhs_norm x (ball_norm x e%:num).
Lemma nbhs_ball_norm (x : V) (eps : {posnum R}) : nbhs x (ball_norm x eps%:num).
Lemma ball_norm_dec x y (e : R) : {ball_norm x e y} + {¬ ball_norm x e y}.
Lemma ball_norm_sym x y (e : R) : ball_norm x e y → ball_norm y e x.
Lemma ball_norm_le x (e1 e2 : R) :
e1 ≤ e2 → ball_norm x e1 `<=` ball_norm x e2.
Let nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs).
Lemma cvg_distP {F : set (set V)} {FF : Filter F} (y : V) :
F --> y ↔ ∀ eps, 0 < eps → \∀ y' \near F, `|y - y'| < eps.
Lemma cvg_dist {F : set (set V)} {FF : Filter F} (y : V) :
F --> y → ∀ eps, eps > 0 → \∀ y' \near F, `|y - y'| < eps.
Lemma nbhs_norm_ball x (eps : {posnum R}) : nbhs_norm x (ball x eps%:num).
End PseudoNormedZmod_numDomainType.
#[global] Hint Resolve normr_ge0 : core.
Arguments cvg_dist {_ _ F FF}.
Lemma cvg_gt_ge T (F : set (set T)) (R : realFieldType) {PF : ProperFilter F}
(u : T → R) a b :
u @ F --> b → (a < b)%R → \∀ n \near F, (a ≤ u n)%R.
Lemma cvg_lt_le T (F : set (set T)) (R : realFieldType) {PF : ProperFilter F}
(u : T → R) c b :
u @ F --> b → (b < c)%R → \∀ n \near F, (u n ≤ c)%R.
Lemma pinfty_ex_gt {R : numFieldType} (m : R) (A : set R) : m \is Num.real →
(\∀ k \near +oo, A k) → exists2 M, m < M & A M.
Lemma pinfty_ex_gt0 {R : numFieldType} (A : set R) :
(\∀ k \near +oo, A k) → exists2 M, M > 0 & A M.
Definition self_sub (K : numDomainType) (V W : normedModType K)
(f : V → W) (x : V × V) : W := f x.1 - f x.2.
Arguments self_sub {K V W} f x /.
Definition fun1 {T : Type} {K : numFieldType} : T → K := fun⇒ 1.
Arguments fun1 {T K} x /.
Definition dominated_by {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}
(h : T → V) (k : K) (f : T → W) (F : set (set T)) :=
F [set x | `|f x| ≤ k × `|h x|].
Definition strictly_dominated_by {T : Type} {K : numDomainType} {V W : pseudoMetricNormedZmodType K}
(h : T → V) (k : K) (f : T → W) (F : set (set T)) :=
F [set x | `|f x| < k × `|h x|].
Lemma sub_dominatedl (T : Type) (K : numFieldType) (V W : pseudoMetricNormedZmodType K)
(h : T → V) (k : K) (F G : set (set T)) : F `=>` G →
(@dominated_by T K V W h k)^~ G `<=` (dominated_by h k)^~ F.
Lemma sub_dominatedr (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
(h : T → V) (k : K) (f g : T → V) (F : set (set T)) (FF : Filter F) :
(\∀ x \near F, `|f x| ≤ `|g x|) →
dominated_by h k g F → dominated_by h k f F.
Lemma dominated_by1 {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
@dominated_by T K _ V fun1 = fun k f F ⇒ F [set x | `|f x| ≤ k].
Lemma strictly_dominated_by1 {T : Type} {K : numFieldType}
{V : pseudoMetricNormedZmodType K} :
@strictly_dominated_by T K _ V fun1 = fun k f F ⇒ F [set x | `|f x| < k].
Lemma ex_dom_bound {T : Type} {K : numFieldType} {V W : pseudoMetricNormedZmodType K}
(h : T → V) (f : T → W) (F : set (set T)) {PF : ProperFilter F}:
(\∀ M \near +oo, dominated_by h M f F) ↔
∃ M, dominated_by h M f F.
Lemma ex_strict_dom_bound {T : Type} {K : numFieldType}
{V W : pseudoMetricNormedZmodType K}
(h : T → V) (f : T → W) (F : set (set T)) {PF : ProperFilter F} :
(\∀ x \near F, h x != 0) →
(\∀ M \near +oo, dominated_by h M f F) ↔
∃ M, strictly_dominated_by h M f F.
Definition bounded_near {T : Type} {K : numFieldType}
{V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) :=
\∀ M \near +oo, F [set x | `|f x| ≤ M].
Lemma boundedE {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
@bounded_near T K V = fun f F ⇒ \∀ M \near +oo, dominated_by fun1 M f F.
Lemma sub_boundedr (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
(F G : set (set T)) : F `=>` G →
(@bounded_near T K V)^~ G `<=` bounded_near^~ F.
Lemma sub_boundedl (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K)
(f g : T → V) (F : set (set T)) (FF : Filter F) :
(\∀ x \near F, `|f x| ≤ `|g x|) → bounded_near g F → bounded_near f F.
Lemma ex_bound {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) {PF : ProperFilter F}:
bounded_near f F ↔ ∃ M, F [set x | `|f x| ≤ M].
Lemma ex_strict_bound {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) {PF : ProperFilter F}:
bounded_near f F ↔ ∃ M, F [set x | `|f x| < M].
Lemma ex_strict_bound_gt0 {T : Type} {K : numFieldType} {V : pseudoMetricNormedZmodType K}
(f : T → V) (F : set (set T)) {PF : Filter F}:
bounded_near f F → exists2 M, M > 0 & F [set x | `|f x| < M].
Notation "[ 'bounded' E | x 'in' A ]" := (bounded_near (fun x ⇒ E) (globally A))
(at level 0, x name, format "[ 'bounded' E | x 'in' A ]").
Notation bounded_set := [set A | [bounded x | x in A]].
Notation bounded_fun := [set f | [bounded f x | x in setT]].
Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T → R) :
bounded_fun a → has_ubound (range a).
Lemma bounded_funN (T : Type) (R : realFieldType) (a : T → R) :
bounded_fun a → bounded_fun (- a).
Lemma bounded_fun_has_lbound (T : Type) (R : realFieldType) (a : T → R) :
bounded_fun a → has_lbound (range a).
Lemma bounded_funD (T : Type) (R : realFieldType) (a b : T → R) :
bounded_fun a → bounded_fun b → bounded_fun (a \+ b).
Lemma bounded_locally (T : topologicalType)
(R : numFieldType) (V : normedModType R) (A : set T) (f : T → V) :
[bounded f x | x in A] → [locally [bounded f x | x in A]].
Notation "k .-lipschitz_on f" := (dominated_by (self_sub id) k (self_sub f))
(at level 2, format "k .-lipschitz_on f") : type_scope.
Definition sub_klipschitz (K : numFieldType) (V W : normedModType K) (k : K)
(f : V → W) (F G : set (set (V × V))) :
F `=>` G → k.-lipschitz_on f G → k.-lipschitz_on f F.
Definition lipschitz_on (K : numFieldType) (V W : normedModType K)
(f : V → W) (F : set (set (V × V))) :=
\∀ M \near +oo, M.-lipschitz_on f F.
Definition sub_lipschitz (K : numFieldType) (V W : normedModType K)
(f : V → W) (F G : set (set (V × V))) :
F `=>` G → lipschitz_on f G → lipschitz_on f F.
Lemma klipschitzW (K : numFieldType) (V W : normedModType K) (k : K)
(f : V → W) (F : set (set (V × V))) {PF : ProperFilter F} :
k.-lipschitz_on f F → lipschitz_on f F.
Notation "k .-lipschitz_ A f" :=
(k.-lipschitz_on f (globally (A `*` A)))
(at level 2, A at level 0, format "k .-lipschitz_ A f").
Notation "k .-lipschitz f" := (k.-lipschitz_setT f)
(at level 2, format "k .-lipschitz f") : type_scope.
Notation "[ 'lipschitz' E | x 'in' A ]" :=
(lipschitz_on (fun x ⇒ E) (globally (A `*` A)))
(at level 0, x name, format "[ 'lipschitz' E | x 'in' A ]").
Notation lipschitz f := [lipschitz f x | x in setT].
Lemma klipschitz_locally (R : numFieldType) (V W : normedModType R)
(k : R) (f : V → W) (A : set V) :
k.-lipschitz_A f → [locally k.-lipschitz_A f].
Lemma lipschitz_locally (R : numFieldType) (V W : normedModType R)
(A : set V) (f : V → W) :
[lipschitz f x | x in A] → [locally [lipschitz f x | x in A]].
Lemma lipschitz_id (R : numFieldType) (V : normedModType R) : 1.-lipschitz (@id V).
Arguments lipschitz_id {R V}.
Section PseudoNormedZMod_numFieldType.
Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).
Lemma norm_hausdorff : hausdorff_space V.
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: norm_hausdorff] : core.
TODO: check if the following lemma are indeed useless
i.e. where the generic lemma is applied,
check that norm_hausdorff is not used in a hard way
Lemma norm_closeE (x y : V): close x y = (x = y).
Lemma norm_close_eq (x y : V) : close x y → x = y.
Lemma norm_cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : V | F --> x].
Lemma norm_cvg_eq (x y : V) : x --> y → x = y.
Lemma norm_lim_id (x : V) : lim x = x.
Lemma norm_cvg_lim {F} {FF : ProperFilter F} (l : V) : F --> l → lim F = l.
Lemma norm_lim_near_cst U {F} {FF : ProperFilter F} (l : V) (f : U → V) :
(\∀ x \near F, f x = l) → lim (f @ F) = l.
Lemma norm_lim_cst U {F} {FF : ProperFilter F} (k : V) :
lim ((fun _ : U ⇒ k) @ F) = k.
Lemma norm_cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U → set V) :
{near F, is_fun f} → is_subset1 [set x : V | f `@ F --> x].
Lemma norm_cvgi_map_lim {U} {F} {FF : ProperFilter F} (f : U → V → Prop) (l : V) :
F (fun x : U ⇒ is_subset1 (f x)) →
f `@ F --> l → lim (f `@ F) = l.
Lemma distm_lt_split (z x y : V) (e : R) :
`|x - z| < e / 2 → `|z - y| < e / 2 → `|x - y| < e.
Lemma distm_lt_splitr (z x y : V) (e : R) :
`|z - x| < e / 2 → `|z - y| < e / 2 → `|x - y| < e.
Lemma distm_lt_splitl (z x y : V) (e : R) :
`|x - z| < e / 2 → `|y - z| < e / 2 → `|x - y| < e.
Lemma normm_leW (x : V) (e : R) : e > 0 → `|x| ≤ e / 2 → `|x| < e.
Lemma normm_lt_split (x y : V) (e : R) :
`|x| < e / 2 → `|y| < e / 2 → `|x + y| < e.
Lemma cvg_distW {F : set (set V)} {FF : Filter F} (y : V) :
(∀ eps, 0 < eps → \∀ y' \near F, `|y - y'| ≤ eps) →
F --> y.
End PseudoNormedZMod_numFieldType.
Section NormedModule_numFieldType.
Variables (R : numFieldType) (V : normedModType R).
Lemma cvg_bounded_real {F : set (set V)} {FF : Filter F} (y : V) :
F --> y →
\∀ M \near +oo, \∀ y' \near F, `|y'| < M.
Lemma cvg_bounded {F : set (set V)} {FF : Filter F} (y : V) :
F --> y → bounded_near id F.
Lemma normrZV (x : V) : x != 0 → `| `| x |^-1 *: x | = 1.
End NormedModule_numFieldType.
Arguments cvg_bounded {_ _ F FF}.
#[global]
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: norm_hausdorff] : core.
Module Export NbhsNorm.
Definition nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs).
End NbhsNorm.
TODO: generalize to R : numFieldType
Section hausdorff.
Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType)
(V : pseudoMetricNormedZmodType R) :
hausdorff_space V.
End hausdorff.
Module Export NearNorm.
Definition near_simpl := (@near_simpl, @nbhs_normE, @filter_from_normE,
@near_nbhs_norm).
Ltac near_simpl := rewrite ?near_simpl.
End NearNorm.
Lemma continuous_cvg_dist {R : numFieldType}
(V W : pseudoMetricNormedZmodType R) (f : V → W) x l :
continuous f → x --> l → ∀ e : {posnum R}, `|f l - f x| < e%:num.
Module Bigminr.
Section bigminr.
Variable (R : realDomainType).
Lemma bigminr_maxr I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i.
Lemma bigminr_mkcond I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i =
\big[minr/x]_(i <- r) (if P i then F i else x).
Lemma bigminr_split I r (P : pred I) (F1 F2 : I → R) x :
\big[minr/x]_(i <- r | P i) (minr (F1 i) (F2 i)) =
minr (\big[minr/x]_(i <- r | P i) F1 i) (\big[minr/x]_(i <- r | P i) F2 i).
Lemma bigminr_idl I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i = minr x (\big[minr/x]_(i <- r | P i) F i).
Lemma bigminrID I r (a P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i =
minr (\big[minr/x]_(i <- r | P i && a i) F i)
(\big[minr/x]_(i <- r | P i && ~~ a i) F i).
Lemma bigminr_seq1 I (i : I) (F : I → R) x :
\big[minr/x]_(j <- [:: i]) F j = minr (F i) x.
Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I → R) x :
\big[minr/x]_(j | j == i) F j = minr (F i) x.
Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I → R) x :
P =1 pred1 i → \big[minr/x]_(j | P j) F j = minr (F i) x.
Lemma bigminrD1 (I : finType) j (P : pred I) (F : I → R) x :
P j → \big[minr/x]_(i | P i) F i
= minr (F j) (\big[minr/x]_(i | P i && (i != j)) F i).
Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I → R) x i0 :
P i0 → \big[minr/x]_(i | P i) F i ≤ F i0.
Lemma bigminr_ler (I : finType) (F : I → R) (i0 : I) x :
\big[minr/x]_i F i ≤ F i0.
Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I → R) x :
reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
(m ≤ \big[minr/x]_(i | P i) F i).
Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I → R) x :
P i0 → F i0 ≤ m → \big[minr/x]_(i | P i) F i ≤ m.
Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I → R) x :
reflect (m < x ∧ ∀ i, P i → m < F i)
(m < \big[minr/x]_(i | P i) F i).
Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I → R) x :
reflect (x ≤ m ∨ exists2 i, P i & F i ≤ m)
(\big[minr/x]_(i | P i) F i ≤ m).
Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I → R) x :
reflect (x < m ∨ exists2 i, P i & F i < m)
(\big[minr/x]_(i | P i) F i < m).
Lemma bigminr_eq_arg (I : finType) i0 (P : pred I) (F : I → R) x :
P i0 → (∀ i, P i → F i ≤ x) →
\big[minr/x]_(i | P i) F i = F [arg min_(i < i0 | P i) F i]%O.
Lemma eq_bigminr (I : finType) i0 (P : pred I) (F : I → R) x :
P i0 → (∀ i, P i → F i ≤ x) →
{i0 | i0 \in I & \big[minr/x]_(i | P i) F i = F i0}.
End bigminr.
Module Exports.
Arguments bigminr_mkcond {R I r}.
Arguments bigminrID {R I r}.
Arguments bigminr_pred1 {R I} i {P F}.
Arguments bigminrD1 {R I} j {P F}.
Arguments bigminr_ler_cond {R I P F}.
Arguments bigminr_ler {R I F}.
Arguments bigminr_inf {R I} i0 {P m F}.
Arguments bigminr_eq_arg {R I} i0 {P F}.
Arguments eq_bigminr {R I} i0 {P F}.
End Exports.
End Bigminr.
Export Bigminr.Exports.
Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType)
(V : pseudoMetricNormedZmodType R) :
hausdorff_space V.
End hausdorff.
Module Export NearNorm.
Definition near_simpl := (@near_simpl, @nbhs_normE, @filter_from_normE,
@near_nbhs_norm).
Ltac near_simpl := rewrite ?near_simpl.
End NearNorm.
Lemma continuous_cvg_dist {R : numFieldType}
(V W : pseudoMetricNormedZmodType R) (f : V → W) x l :
continuous f → x --> l → ∀ e : {posnum R}, `|f l - f x| < e%:num.
Module Bigminr.
Section bigminr.
Variable (R : realDomainType).
Lemma bigminr_maxr I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i.
Lemma bigminr_mkcond I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i =
\big[minr/x]_(i <- r) (if P i then F i else x).
Lemma bigminr_split I r (P : pred I) (F1 F2 : I → R) x :
\big[minr/x]_(i <- r | P i) (minr (F1 i) (F2 i)) =
minr (\big[minr/x]_(i <- r | P i) F1 i) (\big[minr/x]_(i <- r | P i) F2 i).
Lemma bigminr_idl I r (P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i = minr x (\big[minr/x]_(i <- r | P i) F i).
Lemma bigminrID I r (a P : pred I) (F : I → R) x :
\big[minr/x]_(i <- r | P i) F i =
minr (\big[minr/x]_(i <- r | P i && a i) F i)
(\big[minr/x]_(i <- r | P i && ~~ a i) F i).
Lemma bigminr_seq1 I (i : I) (F : I → R) x :
\big[minr/x]_(j <- [:: i]) F j = minr (F i) x.
Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I → R) x :
\big[minr/x]_(j | j == i) F j = minr (F i) x.
Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I → R) x :
P =1 pred1 i → \big[minr/x]_(j | P j) F j = minr (F i) x.
Lemma bigminrD1 (I : finType) j (P : pred I) (F : I → R) x :
P j → \big[minr/x]_(i | P i) F i
= minr (F j) (\big[minr/x]_(i | P i && (i != j)) F i).
Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I → R) x i0 :
P i0 → \big[minr/x]_(i | P i) F i ≤ F i0.
Lemma bigminr_ler (I : finType) (F : I → R) (i0 : I) x :
\big[minr/x]_i F i ≤ F i0.
Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I → R) x :
reflect (m ≤ x ∧ ∀ i, P i → m ≤ F i)
(m ≤ \big[minr/x]_(i | P i) F i).
Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I → R) x :
P i0 → F i0 ≤ m → \big[minr/x]_(i | P i) F i ≤ m.
Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I → R) x :
reflect (m < x ∧ ∀ i, P i → m < F i)
(m < \big[minr/x]_(i | P i) F i).
Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I → R) x :
reflect (x ≤ m ∨ exists2 i, P i & F i ≤ m)
(\big[minr/x]_(i | P i) F i ≤ m).
Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I → R) x :
reflect (x < m ∨ exists2 i, P i & F i < m)
(\big[minr/x]_(i | P i) F i < m).
Lemma bigminr_eq_arg (I : finType) i0 (P : pred I) (F : I → R) x :
P i0 → (∀ i, P i → F i ≤ x) →
\big[minr/x]_(i | P i) F i = F [arg min_(i < i0 | P i) F i]%O.
Lemma eq_bigminr (I : finType) i0 (P : pred I) (F : I → R) x :
P i0 → (∀ i, P i → F i ≤ x) →
{i0 | i0 \in I & \big[minr/x]_(i | P i) F i = F i0}.
End bigminr.
Module Exports.
Arguments bigminr_mkcond {R I r}.
Arguments bigminrID {R I r}.
Arguments bigminr_pred1 {R I} i {P F}.
Arguments bigminrD1 {R I} j {P F}.
Arguments bigminr_ler_cond {R I P F}.
Arguments bigminr_ler {R I F}.
Arguments bigminr_inf {R I} i0 {P m F}.
Arguments bigminr_eq_arg {R I} i0 {P F}.
Arguments eq_bigminr {R I} i0 {P F}.
End Exports.
End Bigminr.
Export Bigminr.Exports.
Section mx_norm.
Variables (K : numDomainType) (m n : nat).
Implicit Types x y : 'M[K]_(m, n).
Definition mx_norm x : K := (\big[maxr/0%:nng]_i `|x i.1 i.2|%:nng)%:num.
Lemma mx_normE x : mx_norm x = (\big[maxr/0%:nng]_i `|x i.1 i.2|%:nng)%:num.
Lemma ler_mx_norm_add x y : mx_norm (x + y) ≤ mx_norm x + mx_norm y.
Lemma mx_norm_eq0 x : mx_norm x = 0 → x = 0.
Lemma mx_norm0 : mx_norm 0 = 0.
Lemma mx_norm_neq0 x : mx_norm x != 0 → ∃ i, mx_norm x = `|x i.1 i.2|.
Lemma mx_norm_natmul x k : mx_norm (x *+ k) = (mx_norm x) *+ k.
Lemma mx_normN x : mx_norm (- x) = mx_norm x.
End mx_norm.
Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) :
mx_norm x = \big[maxr/0]_ij `|x ij.1 ij.2|.
Definition matrix_normedZmodMixin (K : numDomainType) (m n : nat) :=
@Num.NormedMixin _ _ _ (@mx_norm K m.+1 n.+1) (@ler_mx_norm_add _ _ _)
(@mx_norm_eq0 _ _ _) (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).
Canonical matrix_normedZmodType (K : numDomainType) (m n : nat) :=
NormedZmodType K 'M[K]_(m.+1, n.+1) (matrix_normedZmodMixin K m n).
Section matrix_NormedModule.
Variables (K : numFieldType) (m n : nat).
Lemma mx_norm_ball :
@ball _ [pseudoMetricType K of 'M[K]_(m.+1, n.+1)] = ball_ (fun x ⇒ `| x |).
Definition matrix_PseudoMetricNormedZmodMixin :=
PseudoMetricNormedZmodule.Mixin mx_norm_ball.
Canonical matrix_pseudoMetricNormedZmodType :=
PseudoMetricNormedZmodType K 'M[K]_(m.+1, n.+1) matrix_PseudoMetricNormedZmodMixin.
Lemma mx_normZ (l : K) (x : 'M[K]_(m.+1, n.+1)) : `| l *: x | = `| l | × `| x |.
Definition matrix_NormedModMixin := NormedModMixin mx_normZ.
Canonical matrix_normedModType :=
NormedModType K 'M[K]_(m.+1, n.+1) matrix_NormedModMixin.
End matrix_NormedModule.
Section prod_PseudoMetricNormedZmodule.
Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}.
Lemma ball_prod_normE : ball = ball_ (fun x ⇒ `| x : U × V |).
Lemma prod_norm_ball : @ball _ [pseudoMetricType K of U × V] = ball_ (fun x ⇒ `|x|).
Definition prod_pseudoMetricNormedZmodMixin :=
PseudoMetricNormedZmodule.Mixin prod_norm_ball.
Canonical prod_pseudoMetricNormedZmodType :=
PseudoMetricNormedZmodType K (U × V) prod_pseudoMetricNormedZmodMixin.
End prod_PseudoMetricNormedZmodule.
Section prod_NormedModule.
Context {K : numDomainType} {U V : normedModType K}.
Lemma prod_norm_scale (l : K) (x : U × V) : `| l *: x | = `|l| × `| x |.
Definition prod_NormedModMixin := NormedModMixin prod_norm_scale.
Canonical prod_normedModType :=
NormedModType K (U × V) prod_NormedModMixin.
End prod_NormedModule.
Section example_of_sharing.
Variables (K : numDomainType).
Example matrix_triangke m n (M N : 'M[K]_(m.+1, n.+1)) :
`|M + N| ≤ `|M| + `|N|.
Example pair_triangle (x y : K × K) : `|x + y| ≤ `|x| + `|y|.
End example_of_sharing.
Section prod_NormedModule_lemmas.
Context {T : Type} {K : numDomainType} {U V : normedModType K}.
Lemma cvg_dist2P {F : set (set U)} {G : set (set V)}
{FF : Filter F} {FG : Filter G} (y : U) (z : V):
(F, G) --> (y, z) ↔
∀ eps, 0 < eps →
\∀ y' \near F & z' \near G, `| (y, z) - (y', z') | < eps.
Lemma cvg_dist2 {F : set (set U)} {G : set (set V)}
{FF : Filter F} {FG : Filter G} (y : U) (z : V):
(F, G) --> (y, z) →
∀ eps, 0 < eps →
\∀ y' \near F & z' \near G, `|(y, z) - (y', z')| < eps.
End prod_NormedModule_lemmas.
Arguments cvg_dist2 {_ _ _ F G FF FG}.
Normed vector spaces have some continuous functions
that are in fact continuous on pseudoMetricNormedZmodType
Lemma add_continuous {K : numFieldType} {V : pseudoMetricNormedZmodType K} :
continuous (fun z : V × V ⇒ z.1 + z.2).
Global Instance filter_nbhs (K' : numFieldType) (k : K') :
Filter (nbhs k).
Section NVS_continuity_normedModType.
Context {K : numFieldType} {V : normedModType K}.
Lemma natmul_continuous n : continuous (fun x : V ⇒ x *+ n).
Lemma scale_continuous : continuous (fun z : K × V ⇒ z.1 *: z.2).
Arguments scale_continuous _ _ : clear implicits.
Lemma scaler_continuous k : continuous (fun x : V ⇒ k *: x).
Lemma scalel_continuous (x : V) : continuous (fun k : K ⇒ k *: x).
TODO: generalize to pseudometricnormedzmod
Continuity of norm
Lemma norm_continuous : continuous (normr : V → K).
End NVS_continuity_normedModType.
Lemma nearN {R : numFieldType} (a : R) (P : R → Prop) :
(\∀ x \near (- a), P x) ↔ (\∀ x \near a, P (- x)).
Section mule_continuous.
Variable (R : realFieldType).
Lemma mule_continuous (r : R) : continuous (mule r%:E).
End mule_continuous.
Lemma abse_continuous (R : realFieldType) : continuous (@abse R).
Lemma cvg_abse (T : topologicalType) (R : realFieldType) (F : set (set T)) f
(a : \bar R) : Filter F →
f @ F --> a → `|f x|%E @[x --> F] --> `|a|%E.
Lemma is_cvg_abse (T : topologicalType) (R : realFieldType) (F : set (set T))
(f : T → \bar R) : Filter F →
cvg (f @ F) → cvg ((abse \o f : T → \bar R) @ F).
Lemma cvg_dist0 {U} {K : numFieldType} {V : normedModType K}
{F : set (set U)} {FF : Filter F} (f : U → V) :
(fun x ⇒ `|f x|) @ F --> (0 : K)
→ f @ F --> (0 : V).
Section NVS_continuity_mul.
Context {K : numFieldType}.
Lemma mul_continuous : continuous (fun z : K × K ⇒ z.1 × z.2).
Lemma mulrl_continuous (x : K) : continuous ( *%R x).
Lemma mulrr_continuous (y : K) : continuous ( *%R^~ y).
Lemma inv_continuous (x : K) : x != 0 → {for x, continuous GRing.inv}.
End NVS_continuity_mul.
Section cvg_composition.
Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
Context (F : set (set T)) {FF : Filter F}.
Implicit Types (f g : T → V) (s : T → K) (k : K) (x : T) (a b : V).
Lemma cvgN f a : f @ F --> a → (- f) @ F --> - a.
Lemma is_cvgN f : cvg (f @ F) → cvg (- f @ F).
Lemma is_cvgNE f : cvg ((- f) @ F) = cvg (f @ F).
Lemma cvgMn f n a : f @ F --> a → ((@GRing.natmul _)^~n \o f) @ F --> a *+ n.
Lemma is_cvgMn f n : cvg (f @ F) → cvg (((@GRing.natmul _)^~n \o f) @ F).
Lemma cvgD f g a b : f @ F --> a → g @ F --> b → (f + g) @ F --> a + b.
Lemma is_cvgD f g : cvg (f @ F) → cvg (g @ F) → cvg (f + g @ F).
Lemma cvgB f g a b : f @ F --> a → g @ F --> b → (f - g) @ F --> a - b.
Lemma is_cvgB f g : cvg (f @ F) → cvg (g @ F) → cvg (f - g @ F).
Lemma is_cvgDlE f g : cvg (g @ F) → cvg ((f + g) @ F) = cvg (f @ F).
Lemma is_cvgDrE f g : cvg (f @ F) → cvg ((f + g) @ F) = cvg (g @ F).
Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) → g @ F --> a → f @ F --> a.
Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) → f @ F --> a.
Lemma cvgZ s f k a : s @ F --> k → f @ F --> a →
s x *: f x @[x --> F] --> k *: a.
Lemma is_cvgZ s f : cvg (s @ F) →
cvg (f @ F) → cvg ((fun x ⇒ s x *: f x) @ F).
Lemma cvgZl s k a : s @ F --> k → s x *: a @[x --> F] --> k *: a.
Lemma is_cvgZl s a : cvg (s @ F) → cvg ((fun x ⇒ s x *: a) @ F).
Lemma cvgZr k f a : f @ F --> a → k \*: f @ F --> k *: a.
Lemma is_cvgZr k f : cvg (f @ F) → cvg (k *: f @ F).
Lemma is_cvgZrE k f : k != 0 → cvg (k *: f @ F) = cvg (f @ F).
Lemma cvg_norm f a : f @ F --> a → `|f x| @[x --> F] --> (`|a| : K).
Lemma is_cvg_norm f : cvg (f @ F) → cvg ((Num.norm \o f : T → K) @ F).
End cvg_composition.
Section cvg_composition_ereal.
Context (R : realFieldType) {T : topologicalType}.
Context (F : set (set T)) {FF : Filter F}.
Local Open Scope ereal_scope.
Implicit Types (f : T → \bar R) (g : T → R) (x y : \bar R) (r : R).
Lemma ereal_cvgN f x : f @ F --> x → (-%E \o f @ F) --> - x.
Lemma ereal_is_cvgN f : cvg (f @ F) → cvg ((-%E \o f) @ F).
Lemma ereal_cvgrM f x y : y \is a fin_num →
f @ F --> x → (fun n ⇒ y × f n) @ F --> y × x.
Lemma ereal_is_cvgrM f y : y \is a fin_num →
cvg (f @ F) → cvg ((fun n ⇒ y × f n) @ F).
Lemma ereal_cvgMr f x y : y \is a fin_num →
f @ F --> x → (fun n ⇒ f n × y) @ F --> x × y.
Lemma ereal_is_cvgMr f y : y \is a fin_num →
cvg (f @ F) → cvg ((fun n ⇒ f n × y) @ F).
End cvg_composition_ereal.
Section cvg_composition_field.
Context {K : numFieldType} {T : topologicalType}.
Context (F : set (set T)) {FF : Filter F}.
Implicit Types (f g : T → K) (a b : K).
Lemma cvgM f g a b : f @ F --> a → g @ F --> b → (f × g) @ F --> a × b.
Lemma cvgMl f a b : f @ F --> a → (f x × b) @[x --> F] --> a × b.
Lemma cvgMr g a b : g @ F --> b → (a × g x) @[x --> F] --> a × b.
Lemma is_cvgM f g : cvg (f @ F) → cvg (g @ F) → cvg (f × g @ F).
Lemma is_cvgMr g a (f := fun⇒ a) : cvg (g @ F) → cvg (f × g @ F).
Lemma is_cvgMrE g a (f := fun⇒ a) : a != 0 → cvg (f × g @ F) = cvg (g @ F).
Lemma is_cvgMl f a (g := fun⇒ a) : cvg (f @ F) → cvg (f × g @ F).
Lemma is_cvgMlE f a (g := fun⇒ a) : a != 0 → cvg (f × g @ F) = cvg (f @ F).
Lemma cvgV f a : a != 0 → f @ F --> a → (f x)^-1 @[x --> F] --> a^-1.
Lemma is_cvgV f : lim (f @ F) != 0 → cvg (f @ F) → cvg ((fun x ⇒ (f x)^-1) @ F).
End cvg_composition_field.
Section limit_composition_normedmod.
Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
Context (F : set (set T)) {FF : ProperFilter F}.
Implicit Types (f g : T → V) (s : T → K) (k : K) (x : T) (a : V).
Lemma limN f : cvg (f @ F) → lim (- f @ F) = - lim (f @ F).
Lemma limD f g : cvg (f @ F) → cvg (g @ F) →
lim (f + g @ F) = lim (f @ F) + lim (g @ F).
Lemma limB f g : cvg (f @ F) → cvg (g @ F) →
lim (f - g @ F) = lim (f @ F) - lim (g @ F).
Lemma limZ s f : cvg (s @ F) → cvg (f @ F) →
lim ((fun x ⇒ s x *: f x) @ F) = lim (s @ F) *: lim (f @ F).
Lemma limZl s a : cvg (s @ F) →
lim ((fun x ⇒ s x *: a) @ F) = lim (s @ F) *: a.
Lemma limZr k f : cvg (f @ F) → lim (k *: f @ F) = k *: lim (f @ F).
Lemma lim_norm f : cvg (f @ F) → lim ((fun x ⇒ `|f x| : K) @ F) = `|lim (f @ F)|.
End limit_composition_normedmod.
Section limit_composition_field.
Context {K : numFieldType} {T : topologicalType}.
Context (F : set (set T)) {FF : ProperFilter F}.
Implicit Types (f g : T → K).
Lemma limM f g : cvg (f @ F) → cvg (g @ F) →
lim (f × g @ F) = lim (f @ F) × lim (g @ F).
Lemma limV f : cvg (f @ F) → lim (f @ F) != 0 → lim ((fun x ⇒ (f x)^-1) @ F) = (lim (f @ F))^-1.
End limit_composition_field.
Section local_continuity.
Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.
Implicit Types (f g : T → V) (s t : T → K) (x : T) (k : K) (a : V).
Lemma continuousN (f : T → V) x :
{for x, continuous f} → {for x, continuous (fun x ⇒ - f x)}.
Lemma continuousD f g x :
{for x, continuous f} → {for x, continuous g} →
{for x, continuous (f + g)}.
Lemma continuousB f g x :
{for x, continuous f} → {for x, continuous g} →
{for x, continuous (f - g)}.
Lemma continuousZ s f x :
{for x, continuous s} → {for x, continuous f} →
{for x, continuous (fun x ⇒ s x *: f x)}.
Lemma continuousZr f k x :
{for x, continuous f} → {for x, continuous (k \*: f)}.
Lemma continuousZl s a x :
{for x, continuous s} → {for x, continuous (fun z ⇒ s z *: a)}.
Lemma continuousM s t x :
{for x, continuous s} → {for x, continuous t} →
{for x, continuous (s × t)}.
Lemma continuousV s x : s x != 0 →
{for x, continuous s} → {for x, continuous (fun x ⇒ (s x)^-1%R)}.
End local_continuity.
Module CompleteNormedModule.
Section ClassDef.
Variable K : numFieldType.
Record class_of (T : Type) := Class {
base : NormedModule.class_of K T ;
mixin : Complete.axiom (PseudoMetric.Pack base)
}.
Definition base2 T (cT : class_of T) : CompletePseudoMetric.class_of K T :=
@CompletePseudoMetric.Class _ _ (@base T cT) (@mixin T cT).
Structure type (phK : phant K) := Pack { sort; _ : class_of sort }.
Variables (phK : phant K) (cT : type phK) (T : Type).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition pack :=
fun bT (b : NormedModule.class_of K T) & phant_id (@NormedModule.class K phK bT) b ⇒
fun mT m & phant_id (@Complete.class mT) (@Complete.Class T b m) ⇒
Pack phK (@Class T b m).
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition normedZmodType := @Num.NormedZmodule.Pack K phK cT xclass.
Definition lmodType := @GRing.Lmodule.Pack K phK cT xclass.
Definition pointedType := @Pointed.Pack cT xclass.
Definition filteredType := @Filtered.Pack cT cT xclass.
Definition topologicalType := @Topological.Pack cT xclass.
Definition uniformType := @Uniform.Pack cT xclass.
Definition pseudoMetricType := @PseudoMetric.Pack K cT xclass.
Definition pseudoMetricNormedZmodType :=
@PseudoMetricNormedZmodule.Pack K phK cT xclass.
Definition normedModType := @NormedModule.Pack K phK cT xclass.
Definition completeType := @Complete.Pack cT xclass.
Definition completePseudoMetricType := @CompletePseudoMetric.Pack K cT xclass.
Definition complete_zmodType := @GRing.Zmodule.Pack completeType xclass.
Definition complete_lmodType := @GRing.Lmodule.Pack K phK completeType xclass.
Definition complete_normedZmodType := @Num.NormedZmodule.Pack K phK completeType xclass.
Definition complete_pseudoMetricNormedZmodType :=
@PseudoMetricNormedZmodule.Pack K phK completeType xclass.
Definition complete_normedModType := @NormedModule.Pack K phK completeType xclass.
Definition completePseudoMetric_lmodType : GRing.Lmodule.type phK :=
@GRing.Lmodule.Pack K phK (CompletePseudoMetric.sort completePseudoMetricType)
xclass.
Definition completePseudoMetric_zmodType : GRing.Zmodule.type :=
@GRing.Zmodule.Pack (CompletePseudoMetric.sort completePseudoMetricType)
xclass.
Definition completePseudoMetric_normedModType : NormedModule.type phK :=
@NormedModule.Pack K phK (CompletePseudoMetric.sort completePseudoMetricType)
xclass.
Definition completePseudoMetric_normedZmodType : Num.NormedZmodule.type phK :=
@Num.NormedZmodule.Pack K phK
(CompletePseudoMetric.sort completePseudoMetricType) xclass.
Definition completePseudoMetric_pseudoMetricNormedZmodType :
PseudoMetricNormedZmodule.type phK :=
@PseudoMetricNormedZmodule.Pack K phK
(CompletePseudoMetric.sort completePseudoMetricType) xclass.
End ClassDef.
Module Exports.
Coercion base : class_of >-> NormedModule.class_of.
Coercion base2 : class_of >-> CompletePseudoMetric.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion pseudoMetricNormedZmodType : type >-> PseudoMetricNormedZmodule.type.
Canonical pseudoMetricNormedZmodType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
Coercion pointedType : type >-> Pointed.type.
Canonical pointedType.
Coercion filteredType : type >-> Filtered.type.
Canonical filteredType.
Coercion topologicalType : type >-> Topological.type.
Canonical topologicalType.
Coercion uniformType : type >-> Uniform.type.
Canonical uniformType.
Coercion pseudoMetricType : type >-> PseudoMetric.type.
Canonical pseudoMetricType.
Coercion normedModType : type >-> NormedModule.type.
Canonical normedModType.
Coercion completeType : type >-> Complete.type.
Canonical completeType.
Coercion completePseudoMetricType : type >-> CompletePseudoMetric.type.
Canonical completePseudoMetricType.
Canonical complete_zmodType.
Canonical complete_lmodType.
Canonical complete_normedZmodType.
Canonical complete_pseudoMetricNormedZmodType.
Canonical complete_normedModType.
Canonical completePseudoMetric_lmodType.
Canonical completePseudoMetric_zmodType.
Canonical completePseudoMetric_normedModType.
Canonical completePseudoMetric_normedZmodType.
Canonical completePseudoMetric_pseudoMetricNormedZmodType.
Notation completeNormedModType K := (type (Phant K)).
Notation "[ 'completeNormedModType' K 'of' T ]" := (@pack _ (Phant K) T _ _ idfun _ _ idfun)
(at level 0, format "[ 'completeNormedModType' K 'of' T ]") : form_scope.
End Exports.
End CompleteNormedModule.
Export CompleteNormedModule.Exports.
Arguments cvg_distW {_ _ F FF}.
Lemma R_complete (R : realType) (F : set (set R)) : ProperFilter F → cauchy F → cvg F.
Canonical R_regular_completeType (R : realType) :=
CompleteType R^o (@R_complete R).
Canonical R_regular_CompleteNormedModule (R : realType) :=
[completeNormedModType R of R^o].
Canonical R_completeType (R : realType) :=
[completeType of R for [completeType of R^o]].
Canonical R_CompleteNormedModule (R : realType) :=
[completeNormedModType R of R].
Section at_left_right.
Variable R : numFieldType.
Definition at_left (x : R) := within (fun u ⇒ u < x) (nbhs x).
Definition at_right (x : R) := within (fun u : R ⇒ x < u) (nbhs x).
Global Instance at_right_proper_filter (x : R) : ProperFilter (at_right x).
Global Instance at_left_proper_filter (x : R) : ProperFilter (at_left x).
End at_left_right.
#[global] Typeclasses Opaque at_left at_right.
TODO: backport to mathcomp in progress
Lemma itvxx d (T : porderType d) (x : T) : `[x, x] =i pred1 x.
Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).
Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ ≤ `[a, b]}.
Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).
Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ ≤ `[a, b]}.
/TODO: backport to mathcomp in progress
Lemma at_right_in_segment (R : realFieldType) (x : R) (P : set R) :
(\∀ e \near at_right (0 : R), {in `[x - e, x + e], ∀ x, P x})
↔ (\near x, P x).
Section cvg_seq_bounded.
Context {K : numFieldType}.
Lemma cvg_seq_bounded {V : normedModType K} (a : nat → V) :
cvg a → bounded_fun a.
End cvg_seq_bounded.
Lemma closure_sup (R : realType) (A : set R) :
A !=set0 → has_ubound A → closure A (sup A).
Lemma near_infty_natSinv_lt (R : archiFieldType) (e : {posnum R}) :
\∀ n \near \oo, n.+1%:R^-1 < e%:num.
Lemma near_infty_natSinv_expn_lt (R : archiFieldType) (e : {posnum R}) :
\∀ n \near \oo, 1 / 2 ^+ n < e%:num.
Lemma limit_pointP (T : archiFieldType) (A : set T) (x : T) :
limit_point A x ↔ ∃ a_ : nat → T,
[/\ a_ @` setT `<=` A, ∀ n, a_ n != x & a_ --> x].
Section open_closed_sets.
Variable R : realFieldType .
Some open sets of [R]
Lemma open_lt (y : R) : open [set x : R| x < y].
Hint Resolve open_lt : core.
Lemma open_gt (y : R) : open [set x : R | x > y].
Hint Resolve open_gt : core.
Lemma open_neq (y : R) : open [set x : R | x != y].
Some closed sets of [R]
Lemma closed_le (y : R) : closed [set x : R | x ≤ y].
Lemma closed_ge (y : R) : closed [set x : R | y ≤ x].
Lemma closed_eq (y : R) : closed [set x : R | x = y].
Definition bound_side d (T : porderType d) (c : bool) (x : itv_bound T) :=
if x is BSide c' _ then c == c' else false.
Lemma interval_open a b : ~~ bound_side true a → ~~ bound_side false b →
open [set x : R^o | x \in Interval a b].
Lemma interval_closed a b : ~~ bound_side false a → ~~ bound_side true b →
closed [set x : R^o | x \in Interval a b].
End open_closed_sets.
#[global] Hint Extern 0 (open _) ⇒ now apply: open_gt : core.
#[global] Hint Extern 0 (open _) ⇒ now apply: open_lt : core.
#[global] Hint Extern 0 (open _) ⇒ now apply: open_neq : core.
#[global] Hint Extern 0 (closed _) ⇒ now apply: closed_ge : core.
#[global] Hint Extern 0 (closed _) ⇒ now apply: closed_le : core.
#[global] Hint Extern 0 (closed _) ⇒ now apply: closed_eq : core.
Section closure_left_right_open.
Variable R : archiFieldType.
Implicit Types z : R.
Lemma closure_gt z : closure ([set x | z < x] : set R) = [set x | z ≤ x].
Lemma closure_lt z : closure ([set x : R | x < z]) = [set x | x ≤ z].
End closure_left_right_open.
Section interval.
Variable R : numDomainType.
Definition is_interval (E : set R) :=
∀ x y, E x → E y → ∀ z, x ≤ z ≤ y → E z.
Lemma is_intervalPlt (E : set R) :
is_interval E ↔ ∀ x y, E x → E y → ∀ z, x < z < y → E z.
Lemma interval_is_interval (i : interval R) : is_interval [set` i].
End interval.
Section open_union_rat.
Variable R : realType.
Implicit Types A U : set R.
Let ointsub A U := [/\ open A, is_interval A & A `<=` U].
Let ointsub_rat U q := [set A | ointsub A U ∧ A (ratr q)].
Let ointsub_rat0 q : ointsub_rat set0 q = set0.
Definition bigcup_ointsub U q := \bigcup_(A in ointsub_rat U q) A.
Lemma bigcup_ointsub0 q : bigcup_ointsub set0 q = set0.
Lemma open_bigcup_ointsub U q : open (bigcup_ointsub U q).
Lemma is_interval_bigcup_ointsub U q : is_interval (bigcup_ointsub U q).
Lemma bigcup_ointsub_sub U q : bigcup_ointsub U q `<=` U.
Lemma open_bigcup_rat U : open U →
U = \bigcup_(q in [set q | ratr q \in U]) bigcup_ointsub U q.
End open_union_rat.
Lemma right_bounded_interior (R : realType) (X : set R) :
has_ubound X → X^° `<=` [set r | r < sup X].
Lemma left_bounded_interior (R : realType) (X : set R) :
has_lbound X → X^° `<=` [set r | inf X < r].
Section interval_realType.
Variable R : realType.
Lemma interval_unbounded_setT (X : set R) : is_interval X →
¬ has_lbound X → ¬ has_ubound X → X = setT.
Lemma interval_left_unbounded_interior (X : set R) : is_interval X →
¬ has_lbound X → has_ubound X → X^° = [set r | r < sup X].
Lemma interval_right_unbounded_interior (X : set R) : is_interval X →
has_lbound X → ¬ has_ubound X → X^° = [set r | inf X < r].
Lemma interval_bounded_interior (X : set R) : is_interval X →
has_lbound X → has_ubound X → X^° = [set r | inf X < r < sup X].
Definition Rhull (X : set R) : interval R := Interval
(if `[< has_lbound X >] then BSide `[< X (inf X) >] (inf X)
else BInfty _ true)
(if `[< has_ubound X >] then BSide (~~ `[< X (sup X) >]) (sup X)
else BInfty _ false).
Lemma Rhull0 : Rhull set0 = `]0, 0[ :> interval R.
Lemma sub_Rhull (X : set R) : X `<=` [set x | x \in Rhull X].
Lemma is_intervalP (X : set R) : is_interval X ↔ X = [set x | x \in Rhull X].
Lemma connected_intervalP (E : set R) : connected E ↔ is_interval E.
End interval_realType.
Section segment.
Variable R : realType.
properties of segments in [R]
Lemma segment_connected (a b : R) : connected `[a, b].
Lemma segment_compact (a b : R) : compact `[a, b].
End segment.
Lemma ler0_addgt0P (R : numFieldType) (x : R) :
reflect (∀ e, e > 0 → x ≤ e) (x ≤ 0).
Lemma IVT (R : realType) (f : R → R) (a b v : R) :
a ≤ b → {within `[a, b], continuous f} →
minr (f a) (f b) ≤ v ≤ maxr (f a) (f b) →
exists2 c, c \in `[a, b] & f c = v.
Local properties in [R]
Topology on [R]²
Lemma locally_2d_align :
forall (P Q : R -> R -> Prop) x y,
( forall eps : {posnum R}, (forall uv, ball (x, y) eps uv -> P uv.1 uv.2) ->
forall uv, ball (x, y) eps uv -> Q uv.1 uv.2 ) ->
{near x & y, forall x y, P x y} ->
{near x & y, forall x y, Q x y}.
Proof.
move=> P Q x y /= K => /locallyP [d _ H].
apply/locallyP; exists d => // uv Huv.
by apply (K d) => //.
Qed.
Lemma locally_2d_1d_const_x :
forall (P : R -> R -> Prop) x y,
locally_2d x y P ->
locally y (fun t => P x t).
Proof.
move=> P x y /locallyP [d _ Hd].
exists d => // z Hz.
by apply (Hd (x, z)).
Qed.
Lemma locally_2d_1d_const_y :
forall (P : R -> R -> Prop) x y,
locally_2d x y P ->
locally x (fun t => P t y).
Proof.
move=> P x y /locallyP [d _ Hd].
apply/locallyP; exists d => // z Hz.
by apply (Hd (z, y)).
Qed.
Lemma locally_2d_1d_strong (P : R -> R -> Prop) (x y : R):
(\near x & y, P x y) ->
\forall u \near x & v \near y,
forall (t : R), 0 <= t <= 1 ->
\forall z \near t, \forall a \near (x + z * (u - x))
& b \near (y + z * (v - y)), P a b.
Proof.
move=> P x y.
apply locally_2d_align => eps HP uv Huv t Ht.
set u := uv.1. set v := uv.2.
have Zm : 0 <= Num.max `|u - x| `|v - y| by rewrite ler_maxr 2!normr_ge0.
rewrite ler_eqVlt in Zm.
case/orP : Zm => Zm.
TODO redo
Lemma locally_2d_1d (P : R -> R -> Prop) x y :
locally_2d x y P ->
locally_2d x y (fun u v => forall t, 0 <= t <= 1 -> locally_2d (x + t * (u - x)) (y + t * (v - y)) P).
Proof.
move/locally_2d_1d_strong.
apply: locally_2d_impl.
apply locally_2d_forall => u v H t Ht.
specialize (H t Ht).
have : locally t (fun z => locally_2d (x + z * (u - x)) (y + z * (v - y)) P) by [ ].
by apply: locally_singleton.
Qed.
TODO redo
Lemma locally_2d_ex_dec :
forall P x y,
(forall x y, P x y \/ ~P x y) ->
locally_2d x y P ->
{d : {posnum R} | forall u v, `|u - x| < d -> `|v - y| < d -> P u v}.
Proof.
move=> P x y P_dec H.
destruct (@locally_ex _ (x, y) (fun z => P (fst z) (snd z))) as [d Hd].
- apply filterE => z. apply/locallyP. exists eps => // pq. rewrite !(RminusE,RmultE,RplusE). move: (Zm). have : Num.max `|u - x| `|v - y| <= 0 by rewrite -(eqP Zm). rewrite ler_maxl => /andP[H1 H2] _. rewrite (_ : u - x = 0); last by apply/eqP; rewrite -normr_le0. rewrite (_ : v - y = 0); last by apply/eqP; rewrite -normr_le0. rewrite !(mulr0,addr0); by apply HP.
- have : Num.max (`|u - x|) (`|v - y|) < eps.
rewrite ltr_maxl; apply/andP; split.
- case: Huv => /sub_ball_abs /=; by rewrite mul1r absrB.
- case: Huv => _ /sub_ball_abs /=; by rewrite mul1r absrB.
- move: H => /locallyP [e _ H]. by apply/locallyP; exists e.
Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) :
compact A → bounded_set A.
Lemma rV_compact (T : topologicalType) n (A : 'I_n.+1 → set T) :
(∀ i, compact (A i)) →
compact [ set v : 'rV[T]_n.+1 | ∀ i, A i (v ord0 i)].
Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n.+1) :
bounded_set A → closed A → compact A.
Section open_closed_sets_ereal.
Variable R : realFieldType (* TODO: generalize to numFieldType? *).
Local Open Scope ereal_scope.
Implicit Types x y : \bar R.
Implicit Types r : R.
Lemma open_ereal_lt y : open [set r : R | r%:E < y].
Lemma open_ereal_gt y : open [set r : R | y < r%:E].
Lemma open_ereal_lt' x y : x < y → ereal_nbhs x (fun u ⇒ u < y).
Lemma open_ereal_gt' x y : y < x → ereal_nbhs x (fun u ⇒ y < u).
Let open_ereal_lt_real r : open (fun x ⇒ x < r%:E).
Lemma open_ereal_lt_ereal x : open [set y | y < x].
Let open_ereal_gt_real r : open (fun x ⇒ r%:E < x).
Lemma open_ereal_gt_ereal x : open [set y | x < y].
Lemma closed_ereal_le_ereal y : closed [set x | y ≤ x].
Lemma closed_ereal_ge_ereal y : closed [set x | y ≥ x].
End open_closed_sets_ereal.
Section ereal_is_hausdorff.
Variable R : realFieldType.
Implicit Types r : R.
Lemma nbhs_image_ERFin (x : R) (X : set R) :
nbhs x X → nbhs x%:E ((fun r ⇒ r%:E) @` X).
Lemma nbhs_open_ereal_lt r (f : R → R) : r < f r →
nbhs r%:E [set y | y < (f r)%:E]%E.
Lemma nbhs_open_ereal_gt r (f : R → R) : f r < r →
nbhs r%:E [set y | (f r)%:E < y]%E.
Lemma nbhs_open_ereal_pinfty r : (nbhs +oo [set y | r%:E < y])%E.
Lemma nbhs_open_ereal_ninfty r : (nbhs -oo [set y | y < r%:E])%E.
Lemma ereal_hausdorff : hausdorff_space (ereal_topologicalType R).
End ereal_is_hausdorff.
#[global]
Hint Extern 0 (hausdorff_space _) ⇒ solve[apply: ereal_hausdorff] : core.
Lemma EFin_lim (R : realType) (f : nat → R) : cvg f →
lim (EFin \o f) = (lim f)%:E.
Section limit_composition_ereal.
Context {R : realFieldType} {T : topologicalType}.
Context (F : set (set T)) {FF : ProperFilter F}.
Local Open Scope ereal_scope.
Implicit Types (f : T → \bar R) (g : T → R) (x : \bar R) (r : R).
Lemma ereal_limrM f y : y \is a fin_num → cvg (f @ F) →
lim ((fun n ⇒ y × f n) @ F) = y × lim (f @ F).
Lemma ereal_limMr f y : y \is a fin_num → cvg (f @ F) →
lim ((fun n ⇒ f n × y) @ F) = lim (f @ F) × y.
Lemma ereal_limN f : cvg (f @ F) → lim ((-%E \o f) @ F) = - lim (f @ F).
End limit_composition_ereal.
Section Shift.
Context {R : zmodType} {T : Type}.
Definition shift (x y : R) := y + x.
Notation center c := (shift (- c)).
Arguments shift x / y.
Lemma comp_shiftK (x : R) (f : R → T) : (f \o shift x) \o center x = f.
Lemma comp_centerK (x : R) (f : R → T) : (f \o center x) \o shift x = f.
Lemma shift0 : shift 0 = id.
Lemma center0 : center 0 = id.
End Shift.
Arguments shift {R} x / y.
Notation center c := (shift (- c)).
Lemma near_shift {K : numDomainType} {R : normedModType K}
(y x : R) (P : set R) :
(\near x, P x) = (\∀ z \near y, (P \o shift (x - y)) z).
Lemma cvg_comp_shift {T : Type} {K : numDomainType} {R : normedModType K}
(x y : R) (f : R → T) :
(f \o shift x) @ y = f @ (y + x).
Section continuous.
Variables (K : numFieldType) (U V : normedModType K).
Lemma continuous_shift (f : U → V) u :
{for u, continuous f} = {for 0, continuous (f \o shift u)}.
Lemma continuous_withinNshiftx (f : U → V) u :
f \o shift u @ 0^' --> f u ↔ {for u, continuous f}.
End continuous.
Section Closed_Ball.
Lemma ball_open (R : numDomainType) (V : normedModType R) (x : V) (r : R) :
0 < r → open (ball x r).
Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V → R)
(x : V) (e : R) := [set y | norm (x - y) ≤ e].
Lemma closed_closed_ball_ (R : realFieldType) (V : normedModType R)
(x : V) (e : R) : closed (closed_ball_ normr x e).
Definition closed_ball (R : numDomainType) (V : pseudoMetricType R)
(x : V) (e : R) := closure (ball x e).
Lemma closed_ballxx (R: numDomainType) (V : pseudoMetricType R) (x : V)
(e : R) : 0 < e → closed_ball x e x.
Lemma closed_ballE (R : realFieldType) (V : normedModType R) (x : V)
(r : R) : 0 < r → closed_ball x r = closed_ball_ normr x r.
Lemma closed_ball_closed (R : realFieldType) (V : normedModType R) (x : V)
(r : R) : 0 < r → closed (closed_ball x r).
Lemma closed_ball_subset (R : realFieldType) (M : normedModType R) (x : M)
(r0 r1 : R) : 0 < r0 → r0 < r1 → closed_ball x r0 `<=` ball x r1.
Lemma nbhs_closedballP (R : realFieldType) (M : normedModType R) (B : set M)
(x : M) : nbhs x B ↔ ∃ (r : {posnum R}), closed_ball x r%:num `<=` B.
Lemma subset_closed_ball (R : realFieldType) (V : normedModType R) (x : V)
(r : R) : 0 < r → ball x r `<=` closed_ball x r.
TBA topology.v once ball_normE is there
Lemma nbhs0_lt (K : numFieldType) (V : normedModType K) e :
0 < e → \∀ x \near nbhs (0 : V), `|x| < e.
Lemma dnbhs0_lt (K : numFieldType) (V : normedModType K) e :
0 < e → \∀ x \near dnbhs (0 : V), `|x| < e.
Lemma nbhs0_le (K : numFieldType) (V : normedModType K) e :
0 < e → \∀ x \near nbhs (0 : V), `|x| ≤ e.
Lemma dnbhs0_le (K : numFieldType) (V : normedModType K) e :
0 < e → \∀ x \near dnbhs (0 : V), `|x| ≤ e.
Lemma interior_closed_ballE (R : realType) (V : normedModType R) (x : V)
(r : R) : 0 < r → (closed_ball x r)^° = ball x r.
Lemma open_nbhs_closed_ball (R : realType) (V : normedModType R) (x : V)
(r : R) : 0 < r → open_nbhs x (closed_ball x r)^°.
End Closed_Ball.
multi-rule bound_in_itv already exists in interval.v, but we
advocate that it should actually have the following statement.
This does not expose the order between interval bounds.
Lemma bound_itvE (R : numDomainType) (a b : R) :
((a \in `[a, b]) = (a ≤ b)) ×
((b \in `[a, b]) = (a ≤ b)) ×
((a \in `[a, b[) = (a < b)) ×
((b \in `]a, b]) = (a < b)) ×
(a \in `[a, +oo[) ×
(a \in `]-oo, a]).
Lemma near_in_itv {R : realFieldType} (a b : R) :
{in `]a, b[, ∀ y, \∀ z \near y, z \in `]a, b[}.
Notation "f @`[ a , b ]" :=
(`[minr (f a) (f b), maxr (f a) (f b)]) : ring_scope.
Notation "f @`[ a , b ]" :=
(`[minr (f a) (f b), maxr (f a) (f b)]%classic) : classical_set_scope.
Notation "f @`] a , b [" :=
(`](minr (f a) (f b)), (maxr (f a) (f b))[) : ring_scope.
Notation "f @`] a , b [" :=
(`](minr (f a) (f b)), (maxr (f a) (f b))[%classic) : classical_set_scope.
Section image_interval.
Variable R : realDomainType.
Implicit Types (a b : R) (f : R → R).
Lemma mono_mem_image_segment a b f : monotonous `[a, b] f →
{homo f : x / x \in `[a, b] >-> x \in f @`[a, b]}.
Lemma mono_mem_image_itvoo a b f : monotonous `[a, b] f →
{homo f : x / x \in `]a, b[ >-> x \in f @`]a, b[}.
Lemma mono_surj_image_segment a b f : a ≤ b →
monotonous `[a, b] f → set_surj `[a, b] (f @`[a, b]) f →
f @` `[a, b] = f @`[a, b]%classic.
Lemma inc_segment_image a b f : f a ≤ f b → f @`[a, b] = `[f a, f b].
Lemma dec_segment_image a b f : f b ≤ f a → f @`[a, b] = `[f b, f a].
Lemma inc_surj_image_segment a b f : a ≤ b →
{in `[a, b] &, {mono f : x y / x ≤ y}} →
set_surj `[a, b] `[f a, f b] f →
f @` `[a, b] = `[f a, f b]%classic.
Lemma dec_surj_image_segment a b f : a ≤ b →
{in `[a, b] &, {mono f : x y /~ x ≤ y}} →
set_surj `[a, b] `[f b, f a] f →
f @` `[a, b] = `[f b, f a]%classic.
Lemma inc_surj_image_segmentP a b f : a ≤ b →
{in `[a, b] &, {mono f : x y / x ≤ y}} →
set_surj `[a, b] `[f a, f b] f →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in `[f a, f b]).
Lemma dec_surj_image_segmentP a b f : a ≤ b →
{in `[a, b] &, {mono f : x y /~ x ≤ y}} →
set_surj `[a, b] `[f b, f a] f →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in `[f b, f a]).
Lemma mono_surj_image_segmentP a b f : a ≤ b →
monotonous `[a, b] f → set_surj `[a, b] (f @`[a, b]) f →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in f @`[a, b]).
End image_interval.
Section LinearContinuousBounded.
Variables (R : numFieldType) (V W : normedModType R).
Lemma linear_boundedP (f : {linear V → W}) : bounded_near f (nbhs (0 : V)) ↔
\∀ r \near +oo, ∀ x, `|f x| ≤ r × `|x|.
Lemma linear_continuous0 (f : {linear V → W}) :
{for 0, continuous f} → bounded_near f (nbhs (0 : V)).
Lemma linear_bounded0 (f : {linear V → W}) :
bounded_near f (nbhs (0 : V)) → {for 0, continuous f}.
Lemma continuousfor0_continuous (f : {linear V → W}) :
{for 0, continuous f} → continuous f.
Lemma linear_bounded_continuous (f : {linear V → W}) :
bounded_near f (nbhs (0 : V)) ↔ continuous f.
Lemma bounded_funP (f : {linear V → W}) :
(∀ r, ∃ M, ∀ x, `|x| ≤ r → `|f x| ≤ M) ↔
bounded_near f (nbhs (0 : V)).
End LinearContinuousBounded.
((a \in `[a, b]) = (a ≤ b)) ×
((b \in `[a, b]) = (a ≤ b)) ×
((a \in `[a, b[) = (a < b)) ×
((b \in `]a, b]) = (a < b)) ×
(a \in `[a, +oo[) ×
(a \in `]-oo, a]).
Lemma near_in_itv {R : realFieldType} (a b : R) :
{in `]a, b[, ∀ y, \∀ z \near y, z \in `]a, b[}.
Notation "f @`[ a , b ]" :=
(`[minr (f a) (f b), maxr (f a) (f b)]) : ring_scope.
Notation "f @`[ a , b ]" :=
(`[minr (f a) (f b), maxr (f a) (f b)]%classic) : classical_set_scope.
Notation "f @`] a , b [" :=
(`](minr (f a) (f b)), (maxr (f a) (f b))[) : ring_scope.
Notation "f @`] a , b [" :=
(`](minr (f a) (f b)), (maxr (f a) (f b))[%classic) : classical_set_scope.
Section image_interval.
Variable R : realDomainType.
Implicit Types (a b : R) (f : R → R).
Lemma mono_mem_image_segment a b f : monotonous `[a, b] f →
{homo f : x / x \in `[a, b] >-> x \in f @`[a, b]}.
Lemma mono_mem_image_itvoo a b f : monotonous `[a, b] f →
{homo f : x / x \in `]a, b[ >-> x \in f @`]a, b[}.
Lemma mono_surj_image_segment a b f : a ≤ b →
monotonous `[a, b] f → set_surj `[a, b] (f @`[a, b]) f →
f @` `[a, b] = f @`[a, b]%classic.
Lemma inc_segment_image a b f : f a ≤ f b → f @`[a, b] = `[f a, f b].
Lemma dec_segment_image a b f : f b ≤ f a → f @`[a, b] = `[f b, f a].
Lemma inc_surj_image_segment a b f : a ≤ b →
{in `[a, b] &, {mono f : x y / x ≤ y}} →
set_surj `[a, b] `[f a, f b] f →
f @` `[a, b] = `[f a, f b]%classic.
Lemma dec_surj_image_segment a b f : a ≤ b →
{in `[a, b] &, {mono f : x y /~ x ≤ y}} →
set_surj `[a, b] `[f b, f a] f →
f @` `[a, b] = `[f b, f a]%classic.
Lemma inc_surj_image_segmentP a b f : a ≤ b →
{in `[a, b] &, {mono f : x y / x ≤ y}} →
set_surj `[a, b] `[f a, f b] f →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in `[f a, f b]).
Lemma dec_surj_image_segmentP a b f : a ≤ b →
{in `[a, b] &, {mono f : x y /~ x ≤ y}} →
set_surj `[a, b] `[f b, f a] f →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in `[f b, f a]).
Lemma mono_surj_image_segmentP a b f : a ≤ b →
monotonous `[a, b] f → set_surj `[a, b] (f @`[a, b]) f →
∀ y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in f @`[a, b]).
End image_interval.
Section LinearContinuousBounded.
Variables (R : numFieldType) (V W : normedModType R).
Lemma linear_boundedP (f : {linear V → W}) : bounded_near f (nbhs (0 : V)) ↔
\∀ r \near +oo, ∀ x, `|f x| ≤ r × `|x|.
Lemma linear_continuous0 (f : {linear V → W}) :
{for 0, continuous f} → bounded_near f (nbhs (0 : V)).
Lemma linear_bounded0 (f : {linear V → W}) :
bounded_near f (nbhs (0 : V)) → {for 0, continuous f}.
Lemma continuousfor0_continuous (f : {linear V → W}) :
{for 0, continuous f} → continuous f.
Lemma linear_bounded_continuous (f : {linear V → W}) :
bounded_near f (nbhs (0 : V)) ↔ continuous f.
Lemma bounded_funP (f : {linear V → W}) :
(∀ r, ∃ M, ∀ x, `|x| ≤ r → `|f x| ≤ M) ↔
bounded_near f (nbhs (0 : V)).
End LinearContinuousBounded.