tvs structure

Co-authored with Reynald Affeldt <reynald.affeldt@aist.go.jp>
Co-authored with Cyril Cohen <cyril.cohen@inria.fr>

Author: mkerjean

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,27 @@
 
 ### Added
 
+- in `tvs.v`:
+  + HB.structure `Tvs`
+  + HB.factory `TopologicalLmod_isTvs`
+  + lemma `nbhs0N`
+  + lemma `nbhsN`
+  + lemma `nbhsT`
+  + lemma `nbhs_add`
+  + lemma nbhs0_scaler
+  + lemma nbhs0_scaler
+  + HB.Instance of a Tvs od R^o
+  + HB.Instance of a Tvs on a product of Tvs
+  
 ### Changed
 
+- in normedtype.v
+  + HB structure `normedModule` now depends on a Tvs
+    instead of a Lmodule
+  + Factory `PseudoMetricNormedZmod_Lmodule_isNormedModule` becomes
+    `PseudoMetricNormedZmod_Tvs_isNormedModule`
+  + Section `prod_NormedModule` now depends on a `numFieldType`
+  
 ### Renamed
 
 ### Generalized

_CoqProject

@@ -31,6 +31,7 @@ theories/separation_axioms.v
 theories/function_spaces.v
 theories/cantor.v
 theories/prodnormedzmodule.v
+theories/tvs.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v

theories/Make

@@ -17,6 +17,7 @@ separation_axioms.v
 function_spaces.v
 cantor.v
 prodnormedzmodule.v
+tvs.v
 normedtype.v
 realfun.v
 sequences.v

theories/charge.v

@@ -91,7 +91,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.

theories/derive.v

@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-Require Import reals signed topology prodnormedzmodule normedtype landau forms.
+Require Import reals signed topology prodnormedzmodule tvs normedtype landau forms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)

theories/exp.v

@@ -4,7 +4,7 @@ From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import mathcomp_extra.
 Require Import reals ereal.
-Require Import signed topology normedtype landau sequences derive realfun.
+Require Import signed topology tvs normedtype landau sequences derive realfun.
 Require Import itv convex.
 
 (**md**************************************************************************)
@@ -229,7 +229,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s).
 apply: cvg_zero => /=.
 suff Cc : limn
     (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)))
-    @[h --> 0^'] --> (0 : R).
+    @[h --> 0^'] --> 0.
   apply: cvg_sub0 Cc.
   apply/cvgrPdist_lt => eps eps_gt0 /=.
   near=> h; rewrite sub0r normrN /=.

theories/ftc.v

@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop .
-Require Import signed reals ereal topology normedtype sequences real_interval.
+Require Import signed reals ereal topology tvs normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun realfun lebesgue_integral.
 Require Import derive charge.
 
@@ -24,7 +24,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -358,7 +358,7 @@ Proof.
 move=> ab intf; pose fab := f \_ `[a, b].
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
-apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x.
+apply/cvgrPdist_le => /= e e0; near=> x.
 rewrite {1}/int /parameterized_integral sub0r normrN.
 have [|xa] := leP a x.
   move=> ax; apply/ltW; move: ax.
@@ -423,7 +423,6 @@ have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
 rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb].
 apply/cvgrPdist_le => /= e e0.
-rewrite near_simpl.
 have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
 near=> x.
 have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW.
@@ -501,7 +500,7 @@ Corollary continuous_FTC2 f F a b : (a < b)%R ->
 Proof.
 move=> ab cf dF F'f.
 pose fab := f \_ `[a, b].
-pose G x : R := (\int[mu]_(t in `[a, x]) fab t)%R.
+pose G x := (\int[mu]_(t in `[a, x]) fab t)%R.
 have iabf : mu.-integrable `[a, b] (EFin \o f).
   by apply: continuous_compact_integrable => //; exact: segment_compact.
 have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}.
@@ -730,7 +729,7 @@ Lemma increasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R ->
 Proof.
 move=> ab incrF cFb GFb.
 apply/cvgrPdist_le => /= e e0.
-have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb.
+have /cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb.
 have := cvg_at_left_within cFb.
 move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb].
 near=> t.
@@ -748,7 +747,7 @@ Lemma decreasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R ->
 Proof.
 move=> ab decrF cFa GFa.
 apply/cvgrPdist_le => /= e e0.
-have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa.
+have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa.
 have := cvg_at_right_within cFa.
 move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa].
 near=> t.
@@ -766,7 +765,7 @@ Lemma decreasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R ->
 Proof.
 move=> ab decrF cFb GFb.
 apply/cvgrPdist_le => /= e e0.
-have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb.
+have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb.
 have := cvg_at_left_within cFb. (* different point from gt0 version *)
 move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb].
 near=> t.
@@ -863,7 +862,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
       exact: decreasing_image_oo.
     * have : -%R F^`() @ x --> (- f x)%R.
         by rewrite -fE//; apply: cvgN; exact: cF'.
-      apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl.
+      apply: cvg_trans; apply: near_eq_cvg.
       apply: (@open_in_nearW _ _ `]a, b[) ; last by rewrite inE.
         exact: interval_open.
       by move=> z; rewrite inE/= => zab; rewrite fctE fE.
@@ -978,7 +977,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last.
     by case: Fab => + _ _; exact.
   rewrite -derive1E.
   have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg.
-  rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//.
+  near=> y; rewrite fctE !derive1E deriveN//.
   by case: Fab => + _ _; apply; near: y; exact: near_in_itv.
 - by move=> x y xab yab yx; rewrite ltrN2 incrF.
 - by [].

theories/lebesgue_integral.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
-Require Import signed reals ereal topology normedtype sequences real_interval.
+Require Import signed reals ereal topology tvs normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun realfun function_spaces.
 
 (**md**************************************************************************)
@@ -82,7 +82,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope classical_set_scope.
@@ -1671,7 +1671,7 @@ Qed.
 End approximation_sfun.
 
 Section lusin.
-Hint Extern 0  (hausdorff_space _) => (exact: Rhausdorff ) : core.
+Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core.
 Local Open Scope ereal_scope.
 Context (rT : realType) (A : set rT).
 Let mu := [the measure _ _ of @lebesgue_measure rT].

theories/lebesgue_measure.v

@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
-Require Import reals ereal signed topology numfun normedtype function_spaces.
+Require Import reals ereal signed topology numfun tvs normedtype function_spaces.
 From HB Require Import structures.
 Require Import sequences esum measure real_interval realfun exp.
 Require Export lebesgue_stieltjes_measure.
@@ -61,7 +61,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -1708,7 +1708,7 @@ Lemma ae_pointwise_almost_uniform
 Proof.
 move=> mf mg mA Afin [C [mC C0 nC] epspos].
 have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
-    {uniform (A `\` C) `\` B,  f @ \oo --> g}].
+    {uniform (A `\` C) `\` B,  f @\oo --> g}].
   apply: pointwise_almost_uniform => //.
   - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
   - by apply: measurableI => //; exact: measurableC.

theories/normedtype.v

@@ -7,6 +7,7 @@ From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
 Require Export separation_axioms.
+Require Import tvs.
 
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
@@ -799,26 +800,122 @@ Lemma cvgenyP {R : realType} {T} {F : set_system T} {FF : Filter F} (f : T -> na
    (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo).
 Proof. by rewrite cvgeryP cvgrnyP. Qed.
 
-(** Modules with a norm *)
+(** Modules with a norm depending on a numDomain*)
 
-HB.mixin Record PseudoMetricNormedZmod_Lmodule_isNormedModule K V
-    of PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
+HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V
+    of PseudoMetricNormedZmod K V & Tvs K V := {
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
 #[short(type="normedModType")]
 HB.structure Definition NormedModule (K : numDomainType) :=
-  {T of PseudoMetricNormedZmod K T & GRing.Lmodule K T
-   & PseudoMetricNormedZmod_Lmodule_isNormedModule K T}.
+  {T of PseudoMetricNormedZmod K T & Tvs K T
+   & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.
 
-Section regular_topology.
+HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V
+    of PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
+ normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
+}.
 
-Variable R : numFieldType.
+HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
+
+(* NB: These lemmas are done latter with more machinery. They should
+   be be simplified once normedtype is split, and the present section can
+   depend on near lemmas on pseudometricnormedzmodtype ?*)
+Lemma add_continuous : continuous (fun x : V * V => x.1 + x.2).
+Proof.
+move=> [/= x y]; apply/cvg_ballP => e e0 /=.
+rewrite nearE /= -nbhs_ballE  /nbhs_ball /nbhs_ball_ //=.
+exists ((ball x (e/2)),(ball y (e/2))).
+rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0.
+rewrite -ball_normE /= /ball_ /= => xy /= [nx ny].
+rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (@splitr K (e)) ltrD //=.
+Qed.
+
+Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2).
+Proof.
+move=> [/= k x].
+apply/cvg_ballP => e e0 /=. 
+rewrite nearE /= -nbhs_ballE /nbhs_ball /nbhs_ball_ !nbhs_simpl /=.
+near +oo_K=> M.
+pose r := (`|e|/2/M).
+exists ((ball k r),(ball x r)).
+split; apply: nbhsx_ballx; rewrite ?divr_gt0 ?normr_gt0 ?lt0r_neq0 //.
+rewrite -ball_normE /ball /= => lz /= [nk nx]; rewrite -?(scalerBr, scalerBl).
+have := @ball_split _ _ (k *: lz.2)  (k*: x)  (lz.1 *: lz.2) `|e|.
+rewrite -ball_normE /= real_lter_normr ?gtr0_real //. 
+have -> :  (normr (k *: x - lz.1 *: lz.2) < - e) = false
+  by rewrite ltr_nnorml // oppr_le0 ltW.
+rewrite Bool.orb_false_r => T;apply: T; rewrite -?(scalerBr, scalerBl) normrZ.
+rewrite (@le_lt_trans _ _ (M * `|x - lz.2|)) ?ler_wpM2r -?ltr_pdivlMl //.
+rewrite mulrC //.
+rewrite (@le_lt_trans _ _ (`|k - lz.1| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
+rewrite (@le_trans _ _ (normr (lz.2) + normr x)) // ?lerDl ?normr_ge0 //.
+move: nx; rewrite /r => nx. 
+have H: normr lz.2 <= normr x + `|e|/2/M.
+   have -> : lz.2 = x - (x -lz.2) by rewrite opprB addrCA subrr addr0.
+   rewrite (@le_trans _ _ (normr (x) + normr (x - lz.2))) // ?ler_normB ?lerD // ltW //.
+rewrite (@le_trans _ _ ((normr x + `|e| / 2 / M) + (normr x))) ?lerD // addrC.
+(*rewrite addrAC.*)
+have H0: M = M^-1 * (M *  M). rewrite mulrA mulVf ?mul1r // ?lt0r_neq0 //.
+rewrite [X in (_ <= X)]H0.
+have -> : (normr x + (normr x + `|e| / 2 / M)) =
+           M^-1 * ( M * (normr x + normr x)  + `|e| / 2).
+   by rewrite mulrDr mulrA mulVf ?mul1r  ?lt0r_neq0 // mulrC addrA.
+rewrite  ler_wpM2l // ?invr_ge0 // ?ltW // -ltrBrDl -mulrBr. 
+apply: ltr_pM; rewrite ?ltrBrDl //.
+Unshelve. all: by end_near.
+Qed.
+
+Lemma locally_convex : exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B.
+Proof.
+exists [set B | exists x, exists r, B = ball x r].
+  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
+  rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
+  have -> :  x = l *: x + (1-l) *: x
+    by rewrite scalerBl addrCA subrr addr0 scale1r.
+  have -> : (l *: x + (1 - l) *: x) - (l *: z + (1 - l) *: y)
+           = (l *: (x-z) + (1 - l) *: (x - y)).
+    rewrite opprD addrCA addrA addrA -!scalerN -scalerDr [X in l*:X]addrC.
+    by rewrite -addrA -scalerDr.
+  rewrite (@le_lt_trans _ _ ( `|l| * `|x - z| + `|1 - l| * `|x - y|)) //.
+    by rewrite -!normrZ ?ler_normD //.
+    rewrite (@lt_le_trans _ _ ( `|l| * r + `|1 - l| * r )) //.
+    rewrite ltr_leD //.
+    rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?lt0r_neq0 //.
+    rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE;
+    by apply/eqP =>  H; move: l1; rewrite H // lt_def => /andP [] /eqP //=.
+  have -> : normr (1 -l) = 1 - normr l.
+    by move/ltW/normr_idP: l0 => ->; move/ltW/normr_idP: l1 => ->.
+  by rewrite -mulrDl addrCA subrr addr0 mul1r.
+split =>  /=.
+  move => B [x] [r] ->; rewrite openE -!ball_normE /interior=> y /= bxy.
+  rewrite -nbhs_ballE  /nbhs_ball /nbhs_ball_ /filter_from //=.
+  exists (r - (normr (x - y) )); first by rewrite subr_gt0.
+  move=> z; rewrite -ball_normE /= ltrBrDr addrC => H.
+  rewrite /= (le_lt_trans (ler_distD y _ _)) //.
+rewrite /filter_from /= => x B.
+rewrite -nbhs_ballE  /nbhs_ball /nbhs_ball_ /filter_from //=.
+move=> [r] r0 Bxr /=.
+rewrite nbhs_simpl /=; exists (ball x r) => //; split; last by apply: ballxx.
+by exists x; exists r.
+Qed.
+
+HB.instance Definition _ :=
+ Uniform_isTvs.Build K V add_continuous scale_continuous locally_convex.
+
+HB.instance Definition _ :=
+  PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.
+
+HB.end.
 
+Section regular_topology.
+Variable R : numFieldType.
 HB.instance Definition _ := Num.NormedZmodule.on R^o.
+
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl.
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _).
+  PseudoMetricNormedZmod_Tvs_isNormedModule.Build R R^o (@normrM _).
 
 End regular_topology.
 
@@ -2364,14 +2461,14 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type
 End prod_PseudoMetricNormedZmodule.
 
 Section prod_NormedModule.
-Context {K : numDomainType} {U V : normedModType K}.
+Context {K : numFieldType} {U V : normedModType K}.
 
 Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
 Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed.
 
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K (U * V)%type
-    prod_norm_scale.
+  PseudoMetricNormedZmod_Tvs_isNormedModule.Build K (U * V)%type
+  prod_norm_scale.
 
 End prod_NormedModule.