Library struct_top

Require Import Classical_Prop IndefiniteDescription Classical_Pred_Type.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
Require Import fintype bigop binomial ssralg matrix ssrnum complex.
Require Import mxstructure ssrcomplements jordan.
Require Import C_complements big_minmax set_theory mxorder.

We define in this file an abstract structure of topological space and of metric space. Then we instantiate a metric and a topology :

on each structure define in the file ssrnum.v of SSReflect library
on matrices.

This file also contains some general theory about the above structures. In particular he contains the Bolzano-Weirstrass theorem.

ArchiDomain structure

archiDomainType == it is not exactly an archimedean field. It is more precisely a numFieldType that satisfies the archimedean axiom. ArchiDomainType T r == packs the archimedean axiom r into an archiDomainType. The carrier T must have a numFieldtype structure. [archiDomainType of T for S ] == T-clone of the archiDomainType structure S. [archiDomainType of T] == clone of a canonical archiDomainType structure on T.

Topological space

topologyType == interface for an topological space. TopologyType T m == packs the topology mixin into an topologyType. [topologyType of T for S ] == T-clone of the topologyType structure S. [topologyType of T] == clone of a canonical topologyType structure on T. open A == A is an open set. A° == the interior of the set A. closed A == A is a closed set. /A == the closure of A. boundary A == the boundary of the set A. neighbourhood V x == V is a neighbourhood of the point x. neigh_open V x == V is an open neighbourhood of x. separated T == the topologcal space T is separated. open_family f == all sets of the family f are open. quasi_compact K == K is quasi compact (like a compact but not in a separated space). compact K == K is a compact set. Un >->> l == the sequence Un (of type nat -> T, where T is a topological space) converges towards l. cluster_point Un l == l is a cluster point of the sequence Un. continue_pt f x == the function f is continue at point x. continue f == the function f is continue.

Metric space

espMetType R == interface for an metric space where the distance has return type R. EspMetType R T m == packs the metric mixin into an espMetType. [espMetType R of T for S ] == T-clone of the espMetType structure S. [espMetType R of T] == clone of a canonical espMetType structure on T. {posD T} == the type of positive elements of numDomainType T. PosD == the constructor of type {posD T}. it takes as argument a proof that a number is positive. posn == it is the projection of {posD T} to T. posn_gt0 r == a proof that posn r is positive. pceil r == the ceiling of (r : {posD T}). pfloor r == the floor of (r : {posD T}). 'B(x,r) == the open ball of center x : E and of radius r : {posD R}, where E has type espMetType R bounded A == the set A is bounded.

Matrix norm

can_norm == a structure for generic canonical norm over matrices. norm8 M == the infinity norm of M. ||M : norm| == the canonical norm "norm" of the matrix M. Here norm is an instance of the can_norm structure.

Set Implicit Arguments.
Import Prenex Implicits.

Reserved Notation "{ 'posD' T }" (at level 0, format "{ 'posD' T }").

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Module ArchimedeanDomain.

Local Open Scope ring_scope.

Section ClassDef.
Local Notation num_for T b := (@Num.NumDomain.Pack T b T).
Record class_of R :=
  Class { base : Num.NumField.class_of R;
             _ : Num.archimedean_axiom (num_for R base) }.
Local Coercion base : class_of >-> Num.NumField.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : Num.archimedean_axiom (num_for T b0)) :=
  fun bT b & phant_id (Num.NumField.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @Num.NumDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition numFieldType := @Num.NumField.Pack cT xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Num.NumField.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 ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> Num.NumDomain.type.
Canonical numDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> Num.NumField.type.
Canonical numFieldType.
Notation archiDomainType := type.
Notation ArchiDomainType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'archiDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'archiDomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'archiDomainType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'archiDomainType' 'of' T ]") : form_scope.
End Exports.

End ArchimedeanDomain.
Export ArchimedeanDomain.Exports.

Module Import Internals.

Fact archiD_bound_subproof (R : archiDomainType) : Num.archimedean_axiom R.

End Internals.

Module Import ExtraDef.

Definition archiD_bound {R} x := sval (sigW (@archiD_bound_subproof R x)).

End ExtraDef.

Notation boundD := archiD_bound.

Section Theory.

Section ArchimedeanFieldTheory.

Local Open Scope ring_scope.

Variables (F : archiDomainType) (x : F).

Lemma archiD_boundP : 0 <= x -> x < (boundD x )%:R.

End ArchimedeanFieldTheory.

Lemma archi_axiom (T : archiFieldType) : Num.archimedean_axiom T.

Canonical Structure archi_archi (T : archiFieldType) :=
  ArchiDomainType T (@archi_axiom T).

End Theory.

Module Topology.

Structure mixin_of (T_Space : Type) : Type := Mixin
  {
    open : (T_Space -> Prop) -> Prop;
    _ : open {ø : T_Space };
    _ : open {full : T_Space };
    _ : forall (E : (T_Space -> Prop) -> Prop), E <s open ->
          open (union_s E id);
    _ : forall A B, open A -> open B -> open (inter A B);
    _ : forall A B, A =s B -> (open A <-> open B)
  }.

Section ClassDef.

Notation class_of := mixin_of (only parsing).

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.

Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition pack c := @Pack T c T.
Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.

Notation topologyType := type.
Notation TopologyMixin := Mixin.
Notation TopologyType T m := (@pack T m).
Notation " [ 'topologyType' 'of' T ] " := (@clone T _ _ id idfun)
  (at level 0, format "[ 'topologyType' 'of' T ]") : form_scope.
Notation "[ 'topologyType' 'of' T 'for' C ]" := (@clone T C _ id idfun)
  (at level 0, format "[ 'topologyType' 'of' T 'for' C ]") : form_scope.

End Exports.
End Topology.
Export Topology.Exports.

Section TopologyTheory.

Variable T : topologyType.

Canonical Structure Top_eqType := Eval hnf in EqType T (T_eqMixin T).

Definition open := Topology.open (Topology.class T).

Add Morphism open with signature (@eqset T ) ==> iff as open_mor.

Lemma empty_in_open : open {ø : T }.

Lemma full_in_open : open {full : T }.

Lemma union_open : forall (E : (T -> Prop) -> Prop), E <s open ->
      open (union_s E (@id (T ->Prop))).

Lemma inter_open : forall A B, open A -> open B -> open (inter A B).

Lemma union_open2 (E: (T -> Prop) -> Prop) F :
  (forall A, A 'in E -> open (F A)) -> open (union_s E F).

Definition interior (A : T -> Prop) :=
  union_s (fun B => open B /\ B <s A) id.

Notation "A °" := (interior A) (at level 0, no associativity).

Lemma int_go A B : open A -> A <s B -> A <s B °.

Lemma open_int A : open A °.

Lemma int_in A : A ° <s A.

Add Morphism interior with signature (@eqset T ) ==> (@eqset T )
  as interior_mor.

Lemma int_open_eq A : open A <-> A <s A °.

Lemma int_inter A B : (inter A B )° =s inter A ° B °.

Lemma int_union A B : union A ° B ° <s (union A B )° .

Definition closed (A : T -> Prop) : Prop := open (A ^c).

Add Morphism closed with signature (@eqset T ) ==> iff as closed_mor.

Lemma empty_closed : closed {ø : T }.

Lemma full_closed : closed {full : T }.

Lemma inter_closed (E : (T -> Prop) -> Prop) :
  (forall A, A 'in E -> closed A) -> closed (inter_s E id).

Lemma union_closed A B : closed A -> closed B -> closed (union A B).

Definition closure (A : T -> Prop) := inter_s (fun B => closed B /\ A <s B) id.

Notation "/ A" := (closure A).

Lemma closure_lc A B : closed A -> B <s A -> /B <s A.

Lemma in_closure A : A <s /A.

Lemma closed_closure A : closed (/A).

Add Morphism closure with signature (@eqset T ) ==> (@eqset T ) as closure_mor.

Lemma closure_closed_eq A : closed A <-> /A <s A.

Lemma closure_union A B : /(union A B ) =s union (/A) (/B).

Lemma closure_inter A B : /(inter A B ) <s inter (/A) (/B).

Lemma clsr_cmpl_int A : /(A ^c ) =s (A °)^c .

Lemma int_cmpl_clsr A : (A ^c )° =s (/A )^c.

Definition boundary (A : T -> Prop) := (/A ) \ (A °).

Add Morphism boundary with signature (@eqset T ) ==> (@eqset T ) as boundary_mor.

Lemma partition1 A x : x 'in A -> x 'in A ° \/ boundary A x.

Lemma partition2 A x : x 'in A ^c \/ x 'in A ° \/ boundary A x.

Lemma boundary_eq_compl A : boundary A =s boundary A ^c.

Definition neighbourhood (V : T -> Prop) (x : T) :=
  exists A, [/\ x 'in A , open A & A <s V ].

Definition neigh_open (V : T -> Prop) (x : T) :=
  neighbourhood V x /\ open V.

Lemma in_neigh V x : neighbourhood V x -> x 'in V.

Lemma neighbourhood_full : neighbourhood {full : T } =s {full : T }.

Lemma open_neigh A :
  open A <-> (forall x, x 'in A -> (neighbourhood A x)).

Lemma int_m A : A ° =s fun x => exists V, ((neighbourhood V x ) /\ V <s A ).

Lemma closure_m A :
(/A ) =s
fun x => (forall V, (neighbourhood V x) -> exists y, y 'in (inter V A )).

Definition separated := forall (x y : T), x <> y -> exists V1, exists V2,
[/\ (neighbourhood V1 x ), (neighbourhood V2 y ) &
     (inter V1 V2 ) <s {ø : T }].

Lemma separated_eq : separated <->
  (forall (x y : T), x <> y -> exists V1, exists V2,
[/\ (neigh_open V1 x ), (neigh_open V2 y ) &
     (inter V1 V2 ) <s {ø : T }]).

Lemma fin_inter : forall (s : seq (T -> Prop)),
   (forall g, g \in s -> open g) -> open (inter_seq s).

Definition open_family Ti (f : family T Ti) :=
  forall i, i 'in (ind f ) -> open (f i).

Lemma open_inter_fini (Ti : eqType) (f : finite_family T Ti) :
  open_family f -> open (inter_fam f).

Definition quasi_compact (K : T -> Prop) :=
   forall Ti (f : family T Ti),
   open_family f -> cover K f ->
   exists g : finite_family T Ti , sub_family f g /\ cover K g.

Add Morphism quasi_compact with signature (@eqset T ) ==> iff
  as quasi_compact_mor.

Definition compact (K : T -> Prop) := separated /\ quasi_compact K.

Add Morphism compact with signature (@eqset T ) ==> iff as compact_mor.

Lemma compct_closed K : compact K -> closed K.

Fixpoint ss_opt (T1 : Type) (s : seq (option T1)) :=
    match s with
     | [::]=> [::]
     | x :: s'=> match x with
                     |Some i => i :: ss_opt s'
                     |None => ss_opt s'
                   end
    end.

Lemma in_ss_opt : forall (T1 : eqType) (s : seq (option T1)) (x : T1),
   (Some x ) \in s <-> x \in ss_opt s.

Lemma closed_in_comp K A : compact K -> closed A -> A <s K -> compact A.

End TopologyTheory.

Notation "A °" := (interior A) (at level 0, no associativity).
Notation "/ A" := (closure A).

Section Topology_sequence.

Variable (T : topologyType).

Definition Un_cvg (Un : nat -> T) (l : T) :=
  forall V, (neighbourhood V l) ->
  exists N : nat , forall n, N <= n -> (Un n ) 'in V.
Notation "Un >->> l" := (Un_cvg Un l) (at level 0, no associativity).

Definition cluster_point (Un : nat -> T) (l : T) :=
  forall V, (neighbourhood V l) ->
  forall N : nat, exists n, N <= n /\ (Un n ) 'in V.

Definition cluster_point2 (Un : nat -> T) (l : T) :=
  forall V, (neigh_open V l) ->
  forall N : nat, exists n, N <= n /\ (Un n ) 'in V.

Lemma cluster_point2_eq (Un : nat-> T) :
  cluster_point Un =s cluster_point2 Un.

Lemma cvg_const (a : T) : (fun _ => a ) >->> a.

Lemma cvg_ext (a : T) (U V : nat -> T) :
  V =1 U -> U >->> a -> V >->> a.

Lemma cvg_shift (a : T) (U : nat -> T) k :
   U >->> a <-> (fun i => U (i + k)%N) >->> a.

Lemma cvg_shiftS (U : nat -> T) l :
(fun n => U n .+1 ) >->> l <-> U >->> l.

Definition fam_clstr (Un : nat -> T) (n : nat) (x : T) :=
  exists k, n <= k /\ x = Un k.

Definition cluster_point3 (Un : nat -> T) :=
    inter_fam (mkfamily {full : nat } (fun n x => (/(fam_clstr Un n )) x)).

Lemma cluster_point3_eq Un : cluster_point Un =s cluster_point3 Un.

Lemma lim_unicity Un l1 l2 : (separated T) ->
   Un >->> l1 -> Un >->> l2 -> l1 = l2.

Structure sub_seq : Type := mkss
   {
     phi :> nat -> nat;
     grow : forall m n, (m < n)%N -> (phi m < phi n)%N
   }.

Lemma grow_contra : forall (g : sub_seq) m n, g n <= g m -> n <= m.

Lemma grow_eq : forall g : nat ->nat,
   (forall k, (g k < g k .+1)%N) <-> (forall m n, (m <n)%N -> (g m < g n)%N ).

Lemma ss_min_id : forall (g : sub_seq) n, n <= g n.

Lemma cvg_ss_cvg : forall (Un : nat -> T) (g : sub_seq) l,
   Un >->> l -> (Un \o g ) >->> l.

Lemma ss_cvg (Un : nat -> T) l :
  (exists g : sub_seq , (Un \o g ) >->> l) -> l 'in (cluster_point Un ).

Lemma Bolzano_Weierstrass : forall (Un : nat -> T) K , compact K ->
   (forall n, (Un n ) 'in K) -> exists l, l 'in (cluster_point Un ).

Lemma closed_lim A : closed A ->
(forall (Un : nat -> T) l, (forall n, (Un n ) 'in A) -> Un >->> l -> l 'in A).

End Topology_sequence.

Notation "Un >->> l" := (Un_cvg Un l) (at level 0, no associativity).

Section Topology_function.

Variables T1 T2 : topologyType.

Definition continue_pt (f : T1 -> T2) (x : T1) :=
  forall V', (neighbourhood V' (f x)) ->
  exists V, (neighbourhood V x ) /\ f ^(V ) <s V'.

Definition continue (f : T1 -> T2) := forall x, continue_pt f x.

Lemma continue_open : forall (f : T1 -> T2),
  (continue f <-> forall U, open U -> open f@^-1(U )).

Lemma continue_closed : forall (f : T1 -> T2),
  (continue f <-> forall U, closed U -> closed f@^-1(U )).

Lemma continue_const (x : T2) : continue (fun (_ : T1) => x).

Lemma continue_ext (f g : T1 -> T2) : f =1 g -> continue f -> continue g.

Lemma cont_cmpct f K : separated T2 -> continue f -> compact K -> compact (f ^(K )).

Lemma continue_cvg f : continue f ->
  (forall (Un : nat -> T1) l, Un >->> l -> (f \o Un ) >->> (f l )).

End Topology_function.

Section Topology_function2.

Variables T1 T2 T3 : topologyType.

Lemma continue_id : continue (@id T1).

Lemma continue_comp : forall (f : T1 -> T2) (g : T3 -> T1),
continue f -> continue g -> continue (f \o g).

End Topology_function2.

Module EspMet.

Open Scope ring_scope.

Structure mixin_of (R : numDomainType) (T : Type) := Mixin {
    dist : T -> T -> R;
    _ : forall x y, 0 <= dist x y ;
    _ : forall x y, dist x y = dist y x;
    _ : forall x y, reflect (x =y) (dist x y == 0);
    _ : forall x y z, dist x y <= dist x z + dist z y
   }.

Section ClassDef.

Variable R : numDomainType.

Notation class_of := (mixin_of R) (only parsing).

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.

Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition pack c := @Pack phR T c T.
Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.
Notation espMetType R := (type (Phant R)).
Notation EspMetMixin := Mixin.
Notation EspMetType R T m := (@pack _ (Phant R) T m).
Notation "[ 'espMetMixin' R 'of' T ]" := (class _ : mixin_of R T)
  (at level 0, format "[ 'espMetMixin' R 'of' T ]") : form_scope.
Notation "[ 'espMetType' R 'of' T 'for' C ]" := (@clone _ (Phant R) T C _ idfun id)
  (at level 0, format "[ 'espMetType' R 'of' T 'for' C ]") : form_scope.
Notation "[ 'espMetType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id id)
  (at level 0, format "[ 'espMetType' R 'of' T ]") : form_scope.

End Exports.
End EspMet.
Export EspMet.Exports.

Section positive.

Variable R : numDomainType.
Open Scope ring_scope.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Lemma inv_INR_pos k : (0 : R ) < k .+1 %:R ^-1.

Structure posDomain := PosD { posn :> R ; _ : 0 < posn }.

Definition posDomain_of of phant R := posDomain.

Canonical Structure natmulV_pos k := PosD (inv_INR_pos k).

Fact posn_gt0 (r : posDomain) : 0 < r.

Lemma ler_minl_pos (x y : posDomain) : minr x y <= x.

Lemma ler_minr_pos (x y : posDomain) : minr x y <= y.

Lemma minr_gt0 (x y : R) : 0 < x -> 0 < y -> 0 < minr x y.

Lemma minr_pos (x y : posDomain) : 0 < minr x y.

Canonical Structure posD_minr x y := PosD (minr_pos x y).

Lemma inv_pos (r : posDomain) : 0 < (posn r )^-1.

Canonical Structure posD_inv r := PosD (inv_pos r).

Lemma ltn_ltrV (F : numFieldType) k n :
(k < n)%N = (n .+1 %:R ^-1 < k .+1 %:R ^-1 :> F ).

Lemma lt_eps_le (T : realDomainType) (a b : T) :
  (forall eps, 0 < eps -> a < b + eps) -> a <= b.

Lemma real_lt_eps_le (a b : R) : a \is Num.real ->
  (forall eps, 0 < eps -> a < b + eps) -> a <= b.

End positive.

Notation "{ 'posD' T }" := (posDomain_of (Phant T)).

Hint Resolve posn_gt0.

Section positive_archi.

Variable R : archiDomainType.
Open Scope ring_scope.

Import Num.Theory.
Import Num.Def.

Lemma ex_sub_proof (x : {posD R }) : exists n : nat , x <= n %:R.

Definition pceil (x : {posD R }) := ex_minn (ex_sub_proof x).

Lemma pceilE (x : {posD R }) : (pceil x ).-1 %:R < x <= (pceil x )%:R.

Lemma leq_pceil (x : {posD R }) n : n %:R <= x -> (n <= (pceil x ))%N.

Lemma ex_up_proof (x : {posD R }) : exists n : nat , n %:R <= x.

Definition pfloor (x : {posD R }) := ex_maxn (ex_up_proof x) (@leq_pceil x).

Lemma pfloorE x : (pfloor x )%:R <= x < (pfloor x ).+1 %:R.

End positive_archi.

Section EspMet_Struct.

Variable (R : numDomainType).
Variable E : (espMetType R).

Import Num.Theory.
Import Num.Def.

Open Scope ring_scope.

Notation d := (EspMet.dist (EspMet.class E)).

Lemma dist_pos : forall x y : E, 0 <= d x y.

Lemma dist_sym : forall x y : E, d x y = d y x.

Lemma dist_refl : forall x y : E, reflect (x = y) (d x y == 0).

Lemma dist_tri : forall x y z : E, d x y <= d x z + d z y.

Definition eqmet (x y : E) : bool := (d x y ) == 0.

Lemma eqmetP : Equality.axiom eqmet.

Canonical Structure EspMet_eqMixin := Eval hnf in EqMixin eqmetP.
Canonical Structure EspMet_eqType := Eval hnf in EqType E EspMet_eqMixin.

Definition open_ball (x : E) (r : {posD R }) (y : E) : Prop := d x y < r.
Notation "''B' ( x , r )" := (open_ball x r)
  (at level 8, format "''B' ( x , r )").

Definition open_met (A : E -> Prop) :=
forall x, x 'in A -> exists r, 'B (x ,r ) <s A.

Lemma empty_in_open_met : open_met {ø : E }.

Lemma full_in_open_met : open_met {full : E }.

Lemma union_open_met : forall (S : (E -> Prop) -> Prop), S <s open_met ->
  open_met (union_s S id).

Lemma inter_open_met : forall A B, open_met A -> open_met B ->
   open_met (inter A B).

Lemma ext_open_met : forall A B, A =s B -> (open_met A <-> open_met B).

Definition EspMet_TopMixin := Eval hnf in TopologyMixin
  empty_in_open_met full_in_open_met union_open_met inter_open_met ext_open_met.
Definition EspMet_TopType := Eval hnf in
   TopologyType E EspMet_TopMixin.

Canonical EspMet_TopMixin.
Canonical EspMet_TopType.

End EspMet_Struct.

Notation d := (EspMet.dist (EspMet.class _)).
Notation "''B' ( x , r )" := (open_ball x r)
  (at level 8, format "''B' ( x , r )").

Section EspMet_Theory.

Section numDomainTypeT.

Variable R : numDomainType.
Variable E : (espMetType R).

Notation d := (EspMet.dist (EspMet.class E)).

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Open Scope ring_scope.

Lemma dist_nul x : d x x = 0.

Lemma bxrx (x : E) r : x 'in 'B (x ,r ).

Lemma ball_open : forall (x : E) r, open 'B (x ,r ).

Lemma ball_neigh : forall (x : E) r, neighbourhood 'B (x ,r ) x.

Lemma interior_met : forall (A : E -> Prop),
   A ° =s (fun x=>exists r, 'B (x ,r ) <s A ).

Lemma closure_met : forall (A : E -> Prop) ,
  /A =s (fun x=> forall r, exists y, y 'in (inter 'B (x ,r ) A )).

Definition bounded (A : E -> Prop) :=
  exists r, forall x y, x 'in A -> y 'in A -> y 'in 'B (x ,r ).

Definition bounded2 (A : E -> Prop) : Prop :=
   exists r, exists x, A <s 'B (x ,r ).

Lemma born_eq : forall A, bounded2 A -> bounded A.

Lemma pos : forall (x y : E), x <>y -> 0 < d x y.

Lemma pos_2 : forall (x y : E), x <> y -> 0 < (d x y )/2%:R.

Lemma comp_born : forall (K : E -> Prop), compact K -> bounded K.

End numDomainTypeT.

Section numFieldTypeT.

Variable R : numFieldType.
Variable E : (espMetType R).

Notation d := (EspMet.dist (EspMet.class E)).

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Open Scope ring_scope.

Lemma separated_esp_met : separated (EspMet_TopType E).

End numFieldTypeT.

Section archiFieldTypeT.

Variable R : archiDomainType.
Variable E : (espMetType R).

Notation d := (EspMet.dist (EspMet.class E)).

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Open Scope ring_scope.

Lemma cont_to_discr (r : {posD R }) :
   (PosD (inv_INR_pos _ (pfloor (posD_inv r)).+1) < r).

Lemma int_nat (A : E -> Prop) :
A ° =s (fun x=> exists n : nat , 'B (x ,(PosD (inv_INR_pos _ n))) <s A ).

Lemma closure_nat : forall (A : E -> Prop), /A =s
(fun x=> forall n, exists y, y 'in (inter 'B (x ,(PosD (inv_INR_pos _ n))) A )).

Lemma born_nat A : bounded A <->
  exists n, forall (x y : E), x 'in A -> y 'in A ->
  y 'in 'B (x ,(PosD (ltr0Sn _ n))).

End archiFieldTypeT.

End EspMet_Theory.

Section EspMet_sequence.

Section numDomainTypeTop.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.
Open Scope ring_scope.

Variable R : numDomainType.
Variable E : (espMetType R).

Definition Un_cvg_met (Un : nat -> E) (l : E) :=
  forall (eps : {posD R }), exists N : nat ,
  forall n, (N <= n)%N -> (Un n ) 'in 'B (l ,eps ).

Lemma Un_cvgMT : forall (Un : nat -> E) l, Un_cvg_met Un l <->
  Un >->> l.

End numDomainTypeTop.

Section archiDomainTypeTop.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.
Open Scope ring_scope.

Variable R : archiDomainType.
Variable E : (espMetType R).

Lemma Un_cvg3 : forall (Un : nat -> E) l, Un >->> l <->
  (forall (k : nat), exists N : nat , forall n, (N <= n)%N ->
  (Un n ) 'in 'B (l ,(PosD (inv_INR_pos _ k)))).

Lemma ex_ss_cvg : forall (Un : nat -> E),
  (exists x, exists g: sub_seq , forall (k:nat),
  (Un (g k)) 'in 'B (x ,(PosD (inv_INR_pos _ k)))) ->
  (exists g : sub_seq , exists x, (Un \o g ) >->> x).

Lemma ex_ss_cvg2 : forall (Un : nat -> E) l,
(forall N: nat, forall (k:nat), exists n: nat ,
(N <= n)%N /\ (Un n .+1 ) 'in 'B (l ,(PosD (inv_INR_pos _ k)))) ->
(exists g: sub_seq , (Un \o g ) >->> l).

Lemma clstr_ss_cvg : forall (Un : nat -> E) l, l 'in (cluster_point Un ) ->
  (exists g : sub_seq , (Un \o g ) >->> l).

Lemma lim_closed : forall (A : E -> Prop),
  (forall (Un : nat -> E) l, (forall n, A (Un n)) -> Un >->> l -> A l)
  -> closed A.

End archiDomainTypeTop.
End EspMet_sequence.

Section EspMet_function.

Import Num.Theory.
Import Num.Def.

Open Scope ring_scope.
Variable R R': numDomainType.
Variables E : (espMetType R).
Variables E': (espMetType R').

Definition continue_pt_met (f : E -> E') (x : E) : Prop :=
  forall (r : {posD R'}), exists r' : {posD R }, forall (y : E),
  (y 'in 'B (x ,r')) -> (f y ) 'in 'B (f x ,r ).

Definition continue_met (f : E -> E') : Prop := forall x, continue_pt_met f x.

Lemma continue_ptMT : forall (f : E -> E') (x : E),
  continue_pt_met f x <-> continue_pt f x.

Lemma continueMT : forall (f : E -> E'), continue_met f <-> continue f.

End EspMet_function.

Section nummetrie.
Variable T : numDomainType.

Open Scope ring_scope.

Definition dist_real (x y : T) := `|x - y |.

Lemma dist_real_ge0 x y : 0 <= dist_real x y.

Lemma dist_real_sym x y : dist_real x y = dist_real y x.

Lemma dist_real_refl x y : reflect (x = y) (dist_real x y == 0).

Lemma dist_real_tri x y z : dist_real x y <= dist_real x z + dist_real z y.

Canonical Structure numEspMetMixin :=
  EspMetMixin dist_real_ge0 dist_real_sym dist_real_refl dist_real_tri.
Canonical Structure numEspMetType :=
Eval hnf in EspMetType T T numEspMetMixin.
Canonical Structure numTopologyType :=
Eval hnf in TopologyType T (EspMet_TopMixin numEspMetType).

End nummetrie.

Section canonical.

Canonical Structure numFieldEspMetType (R : numFieldType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure numFieldTopologyType (R : numFieldType) :=
  [topologyType of R for (numTopologyType R )].
Canonical Structure numClosedFieldEspMetType (R : numClosedFieldType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure numClosedFieldTopologyType (R : numClosedFieldType) :=
  [topologyType of R for (numTopologyType R )].
Canonical Structure realEspMetType (R : realDomainType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure realTopologyType (R : realDomainType) :=
  [topologyType of R for (numTopologyType R )].
Canonical Structure realFieldEspMetType (R : realFieldType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure realFieldTopologyType (R : realFieldType) :=
  [topologyType of R for (numTopologyType R )].
Canonical Structure rcfEspMetType (R : rcfType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure rcfTopologyType (R : rcfType) :=
  [topologyType of R for (numTopologyType R )].
Canonical Structure archiDomainEspMetType (R : archiDomainType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure archiDomainTopologyType (R : archiDomainType) :=
  [topologyType of R for (numTopologyType R )].
Canonical Structure archiFieldEspMetType (R : archiFieldType) :=
  [espMetType R of R for (numEspMetType R )].
Canonical Structure archiFieldTopologyType (R : archiFieldType) :=
  [topologyType of R for (numTopologyType R )].

End canonical.

Section Cmetrie.

Variable Rc : rcfType.
Local Notation C := (complex Rc).

Open Scope ring_scope.

Definition dist_C (x y : C) := Re `|x - y |.

Lemma dist_C_ge0 x y : 0 <= dist_C x y.

Lemma dist_C_sym x y : dist_C x y = dist_C y x.

Lemma dist_C_refl x y : reflect (x = y) (dist_C x y == 0).

Lemma dist_C_tri x y z : dist_C x y <= dist_C x z + dist_C z y.

Canonical Structure EspMet_CMixin :=
  EspMetMixin dist_C_ge0 dist_C_sym dist_C_refl dist_C_tri.
Canonical Structure EspMet_C :=
Eval hnf in EspMetType Rc C EspMet_CMixin.
Canonical Structure Esp_Top_C :=
Eval hnf in TopologyType C (EspMet_TopMixin EspMet_C).

End Cmetrie.

Section numdomain.

Variable R : numDomainType.
Open Scope ring_scope.

Lemma cvgN l (U : nat -> R) : ((fun n => - (U n )) >->> - l ) <-> U >->> l.

Lemma cvg_addl a l (U : nat -> R) :
   (fun n => a + U n ) >->> (a + l ) <-> U >->> l .

Lemma cvg_addr a l (U : nat -> R) :
   (fun n => U n + a ) >->> (l + a ) <-> U >->> l .

Lemma cvg_normr0 (f : nat -> R) : (fun k => `|f k |) >->> 0 -> f >->> 0.

Lemma ler0_cvg (U V : nat -> R) :
  (forall n, 0 <= U n <= V n) -> (V >->> 0) -> U >->> 0.

Lemma normr_cvg0 (U V : nat -> R) : (forall n, `|V n | <= U n) ->
  U >->> 0 -> V >->> 0.

Lemma continue_norm : continue (fun (x : R) => `|x |).

Lemma ler_mulr_cvg0 (U V W : nat -> R) : (forall n, `|U n | <= `|V n |) ->
  (fun n => V n * W n ) >->> 0 -> (fun n => U n * W n ) >->> 0.

End numdomain.

Section numfield.

Variable R F1 : numFieldType.
Open Scope ring_scope.

Lemma cvg_mulr (a b : R) (U : nat -> R) : U >->> a ->
(fun k => b * U k ) >->> (b * a ).

Lemma cvg_mull (a b : R) (U : nat -> R) : U >->> a ->
(fun k => U k * b ) >->> (a * b ).

Lemma continue2 (F : numFieldType)
(f : F1 -> F) c (lt0c : 0 < c) x :
continue_pt_met f x <-> forall r, exists r', forall y, (y 'in 'B (x ,r')) ->
(f y ) 'in 'B (f x ,(PosD (mulr_gt0 (posn_gt0 r) lt0c))).

Lemma continueD (F : numFieldType) (f g : F1 -> F) :
continue f -> continue g -> continue (fun x => f x + g x).

Lemma continueM (F : numFieldType) (f g : F1 -> F) :
continue f -> continue g -> continue (fun x => f x * g x).

Lemma continueX (n : nat) : continue (fun (x : F1) => x ^+n).

Lemma cvg_add l l' (U V : nat -> F1) : U >->> l -> V >->> l' ->
  (fun n => U n + V n ) >->> (l + l').

End numfield.

Section realdomain.

Variable R : realDomainType.
Open Scope ring_scope.

Lemma le_cvg_le (a b : R) (U_ : nat -> R) :
(forall k, a <= U_ k) -> (U_ >->> b) -> a <= b.

Lemma lt_cvg_le (a b : R) (U_ : nat -> R) :
(forall k, a < U_ k) -> (U_ >->> b) -> a <= b.

Lemma sandwich (U V W : nat -> R) l : (forall n, U n <= V n <= W n) ->
(U >->> l) -> (W >->> l) -> (V >->> l).

End realdomain.

Section archi.

Variable R : archiDomainType.
Open Scope ring_scope.

Lemma inv_cvg0 : (fun n => (n .+1 %:R ^-1 : R)) >->> 0.

Lemma cvg_lt1 (x : R) : reflect ((fun k => x ^+ k ) >->> 0) (`|x | < 1).

Lemma polyM_exp_cvg0 :
forall i (a : R),`|a | < 1 ->
  (fun x => x %:R ^+ i * a ^+ x ) >->> 0.

End archi.

Section rcf.

Variable R : rcfType.
Open Scope ring_scope.

Lemma cvg_realc (U : nat -> R) :
   U >->> 0 <-> (fun n => (U n )%:C ) >->> 0.

End rcf.

Section Norm.

Section normDef.

Variable R : numDomainType.
Open Scope ring_scope.

Structure can_norm : Type := MNorm {
  anorm : forall p q, 'M [R ]_(p ,q ) -> R;
  pos_norm : forall p q (A : 'M_(p , q )), 0 <= anorm A;
  hom_pos_norm : forall p q (A : 'M_(p , q )) (r : R),
    anorm (r *: A) = `|r | * anorm A;
  trin_ineq_norm : forall p q (A B : 'M_(p , q )),
    anorm (A + B) <= anorm A + anorm B;
  prod_ineq_norm : forall p q r (A : 'M_(p , q )) (B : matrix _ q r),
    anorm (A *m B) <= anorm A * anorm B;
  canonical_norm : forall p q (A : 'M_(p , q ) ) i j, `|A i j | <= anorm A;
  canonical_norm2 : forall p q (A B: 'M_(p , q )),
    (forall i j, `|A i j | <= `|B i j |) -> anorm A <= anorm B
}.

End normDef.

Local Notation "|| A : N |" := (anorm N A)
  (at level 0, A, N at level 99, format "|| A : N |") : ring_scope.

Section normTheory.

Variable R : numDomainType.
Variable p q: nat.
Variable N : can_norm R.

Open Scope ring_scope.

Lemma cnorm0 : || (0: 'M_(p , q )) : N | = 0.

Lemma cnorm_eq0 (A : 'M [R ]_(p ,q )) : (|| A : N | == 0) = (A == 0).

Lemma cnorm_lt0 (A: 'M_(p , q )) : (0 < ||A : N |) = (A != 0).

Lemma cnormN (A: 'M_(p , q )) : || -A : N | = || A : N |.

End normTheory.
End Norm.

Notation "|| A : N |" := (anorm N A)
  (at level 0, A, N at level 99, format "|| A : N |") : ring_scope.

Section Defnorm.

Variable R : numDomainType.

Open Scope ring_scope.

Definition norm8 (m n : nat) (A : 'M [R ]_(m ,n )) :=
   \maxr_i \sum_j `|A i j|.

Lemma norm8_pos (m n : nat) (A : 'M [R ]_(m ,n )) : 0 <= norm8 A.

Lemma norm8_hom p q (A : 'M_(p , q )) (r : R) : norm8 (r *: A) = `|r | * norm8 A.

Lemma norm8_tri p q (A B : 'M_(p , q )) : norm8 (A + B) <= norm8 A + norm8 B.

Lemma norm8M p q r (A : 'M_(p , q )) (B : matrix _ q r) :
  norm8 (A *m B) <= norm8 A * norm8 B.

Lemma norm8_can1 p q (A : 'M_(p , q ) ) i j : `|A i j | <= norm8 A.

Lemma norm8_can2 p q (A B: 'M_(p , q )) :
  (forall i j, `|A i j | <= `|B i j |) -> norm8 A <= norm8 B.

Canonical Structure can_norm8 := MNorm norm8_pos norm8_hom norm8_tri
  norm8M norm8_can1 norm8_can2.

End Defnorm.

Section matrimetrie.

Variable p q : nat.
Variable R : numDomainType.
Let N:= can_norm8 R.

Open Scope ring_scope.

Definition dist_mat (A B : 'M [R ]_(p ,q )) :=
  ||(A - B ) : N |.

Lemma dist_mat_pos (A B : 'M [R ]_(p ,q )) : 0 <= dist_mat A B.

Lemma dist_mat_sym (A B : 'M [R ]_(p ,q )) : dist_mat A B = dist_mat B A.

Lemma dist_mat_refl (A B : 'M [R ]_(p ,q )) : reflect (A = B) (dist_mat A B == 0).

Lemma dist_mat_tri (A B C : 'M [R ]_(p ,q )) :
  dist_mat A B <= dist_mat A C + dist_mat C B.

Canonical Structure EspMet_matMixin :=
   EspMetMixin dist_mat_pos dist_mat_sym dist_mat_refl dist_mat_tri.
Canonical Structure EspMet_mat :=
  EspMetType R ('M [R ]_(p ,q )) EspMet_matMixin.
Canonical Structure EspTop_mat :=
  Eval hnf in TopologyType ('M [R ]_(p ,q )) (EspMet_TopMixin EspMet_mat).

End matrimetrie.

Section mxTheory.

Section numdomainmx.

Variable R : numDomainType.
Open Scope ring_scope.

Local Notation N8 := (can_norm8 R).

Lemma cvg_scale0r m n (A :'M [R ]_(m ,n )) U : A != 0 ->
   (fun k => (U k ) *: A ) >->> 0 -> U >->> 0.

Lemma norm8_col_mx m1 m2 n (A : 'M_(m1 ,n )) (D : 'M_(m2 ,n )) :
  || col_mx A D : N8 | = maxr ||A : N8 | ||D : N8 |.

Lemma norm8_row_mx0l m n1 n2 (A : 'M_(m ,n2 )) :
  || row_mx (0 : 'M_(m ,n1 )) A : N8 | = ||A : N8 |.

Lemma norm8_row_mx0r m n1 n2 (A : 'M_(m ,n1 )) :
  || row_mx A (0 : 'M_(m ,n2 )) : N8 | = ||A : N8 |.

Lemma norm8_blockmxul m1 m2 n1 n2 (A : 'M_(m1 ,n1 )) :
  || block_mx A 0 0 (0 : 'M_(m2 ,n2 )) : N8 | = ||A : N8 |.

Lemma norm8_blockmxdr m1 m2 n1 n2 (A : 'M_(m2 ,n2 )) :
  || block_mx (0 : 'M_(m1 ,n1 )) 0 0 A : N8 | = ||A : N8 |.

Lemma norm8_blockmxuldr m1 m2 n1 n2 (A : 'M_(m1 ,n1 )) (D : 'M_(m2 ,n2 )) :
  || block_mx A 0 0 D : N8 | = maxr ||A : N8 | ||D : N8 |.

Lemma blockmx_cvgul m1 m2 n1 n2 (U : nat -> 'M [R ]_(m1 ,n1 )) (A : 'M_(m1 ,n1 ))
B C (D : 'M_(m2 ,n2 )) :
(U >->> A) -> (fun k => block_mx (U k) B C D ) >->> (block_mx A B C D ).

Lemma blockmx_cvgdr m1 m2 n1 n2 (U : nat -> 'M [R ]_(m2 ,n2 )) (A : 'M_(m1 ,n1 ))
B C (D : 'M_(m2 ,n2 )) :
(U >->> D) -> (fun k => block_mx A B C (U k)) >->> (block_mx A B C D ).

Lemma blockmx_cvguldr m1 m2 n1 n2 (U : nat -> 'M [R ]_(m1 ,n1 ))
(V : nat -> 'M [R ]_(m2 ,n2 )) (A : 'M_(m1 ,n1 )) B C (D : 'M_(m2 ,n2 )) :
(U >->> A) -> (V >->> D) ->
(fun k => block_mx (U k) B C (V k)) >->> (block_mx A B C D ).

Lemma diag_block_mx_cvg s (UF : nat -> forall n, nat -> 'M [R ]_n .+1)
  (F : forall n, nat -> 'M [R ]_n .+1) :
(forall i, (i < size s)%N ->
  (fun k => UF k (nth 0%N s i) i ) >->> (F (nth 0%N s i) i ))
-> (fun k => diag_block_mx s (UF k)) >->> (diag_block_mx s F ).

Lemma conform_mx_cvg m n p q B (U : nat -> 'M [R ]_(m ,n ))
  (V : nat -> 'M [R ]_(p ,q )) A :
m = p -> n = q -> U >->> A ->
(fun k => conform_mx (V k) (U k)) >->> (conform_mx B A ).

End numdomainmx.

Section numfieldmx.

Variable R : numFieldType.
Open Scope ring_scope.

Local Notation N8 := (can_norm8 R).

Lemma mx_cvgP m n (U_ : nat -> 'M_(m ,n )) (A :'M [R ]_(m ,n )) :
  U_ >->> A <-> (forall i j, (fun n => (U_ n) i j ) >->> (A i j )).

Lemma continu_mulr : forall m n p (A : 'M [R ]_(m ,n )),
   continue (fun (B : 'M [R ]_(n ,p )) => A *m B).

Lemma continu_mull : forall m n p (A : 'M [R ]_(n ,p )),
    continue (fun (B : 'M [R ]_(m ,n )) => B *m A ).

End numfieldmx.

Section realfieldmx.

Variable R : realFieldType.
Local Notation N8 := (can_norm8 R).
Open Scope ring_scope.

Lemma lemx_cvg_lemx m n (A B :'M [R ]_(m ,n )) (U_ : nat -> 'M_(m ,n )) :
(forall k, A <=m : U_ k) -> (U_ >->> B) -> A <=m : B.

Lemma ltmx_cvg_lemx m n (A B :'M [R ]_(m ,n )) (U_ : nat -> 'M_(m ,n )) :
(forall k, A <m : U_ k) -> (U_ >->> B) -> A <=m : B.

End realfieldmx.

Section archidomainmx.

Variable R : archiDomainType.
Open Scope ring_scope.

Lemma cvg_jordan_lt1 (lam : R) n : `|lam | < 1 ->
  (fun k => (Jordan_block lam n .+1 )^+ k ) >->> 0.

End archidomainmx.

Section rcfmx.

Variable R : rcfType.

Local Notation "A ^%:C" := (map_mx (real_complex_def (Phant R)) A) (at level 2).
Local Notation C := (complex R).
Local Notation N8 := (can_norm8 R) .
Local Notation NC := (can_norm8 [numDomainType of C ]).

Open Scope ring_scope.

Lemma normc_mx m n (A : 'M_(m ,n )) : ||A ^%:C : NC | = ||A : N8 |%:C.

Lemma cvg_realc_mx m n (U : nat -> 'M_(m ,n )) :
U >->> 0 <-> (fun (n : nat) => (U n )^%:C ) >->> 0.

End rcfmx.

End mxTheory.

This page has been generated by coqdoc