tvs structure (#1300)

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Co-authored-by: Cyril Cohen <cyril.cohen@inria.fr>
Co-authored-by: Zachary Stone <zstonex@gmail.com>

Author: 4 people

CHANGELOG_UNRELEASED.md

@@ -144,13 +144,35 @@
     `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
     `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
 
+- in `tvs.v`:
+  + HB.structure `Tvs`
+  + HB.factory `TopologicalLmod_isTvs`
+  + lemma `nbhs0N`
+  + lemma `nbhsN`
+  + lemma `nbhsT`
+  + lemma `nbhsB`
+  + lemma `nbhs0Z`
+  + lemma `nbhZ`
+  + 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
 
 - in `normedtype.v`:
   + `near_in_itv` -> `near_in_itvoo`
 
+- in normedtype.v
+  + Section `regular_topology` to `standard_topology`
+  
 ### Generalized
 
 - in `lebesgue_integral.v`:

_CoqProject

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

theories/Make

@@ -35,6 +35,7 @@ homotopy_theory/wedge_sigT.v
 separation_axioms.v
 function_spaces.v
 cantor.v
+tvs.v
 normedtype.v
 realfun.v
 sequences.v

theories/charge.v

@@ -92,7 +92,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,8 +2,8 @@
 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.
-From mathcomp Require Import reals signed topology prodnormedzmodule normedtype.
-From mathcomp Require Import landau forms.
+From mathcomp Require Import reals signed topology prodnormedzmodule tvs.
+From mathcomp Require Import normedtype landau forms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)
@@ -788,13 +788,14 @@ by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
 Qed.
 
 Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
-  continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ 0 id.
+  continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id.
 Proof.
 move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
 apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
 rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT.
 rewrite -ler_pdivlMl //.
-suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_max /= lexx.
+suff : `|x| <= k%:num ^-1 * e%:num.
+  by apply: le_trans; rewrite num_le_max /= lexx.
 near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
 by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
 Unshelve. all: by end_near. Qed.
@@ -803,7 +804,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
   continuous (fun p => f p.1 p.2) ->
   continuous (fun q => (f p.1 q.2 + f q.1 p.2)) /\
   (fun q => f q.1 q.2) \o shift p = cst (f p.1 p.2) +
-    (fun q => f p.1 q.2 + f q.1 p.2) +o_ 0 id.
+    (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id.
 Proof.
 move=> fc; split=> [q|].
   by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));

theories/exp.v

@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import mathcomp_extra reals ereal signed.
-From mathcomp Require Import topology normedtype landau sequences derive.
+From mathcomp Require Import topology tvs normedtype landau sequences derive.
 From mathcomp Require Import realfun itv convex.
 
 (**md**************************************************************************)
@@ -228,7 +228,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 signed reals ereal.
-From mathcomp Require Import topology normedtype sequences real_interval.
+From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import esum measure lebesgue_measure numfun realfun.
 From mathcomp Require Import lebesgue_integral 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_itvoo.
 - 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 signed reals ereal topology.
-From mathcomp Require Import normedtype sequences real_interval esum measure.
+From mathcomp Require Import tvs normedtype sequences real_interval esum measure.
 From mathcomp Require Import lebesgue_measure numfun realfun function_spaces.
 
 (**md**************************************************************************)
@@ -96,7 +96,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.
@@ -1775,7 +1775,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 reals ereal signed.
-From mathcomp Require Import topology numfun normedtype function_spaces.
+From mathcomp Require Import topology numfun tvs normedtype function_spaces.
 From HB Require Import structures.
 From mathcomp Require Import sequences esum measure real_interval realfun exp.
 From mathcomp 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.
@@ -1709,7 +1709,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.