From 0f50886060e5b4c1069b287d0c2f4d7a5ad28b94 Mon Sep 17 00:00:00 2001 From: Marie Kerjean <43064157+mkerjean@users.noreply.github.com> Date: Thu, 14 Nov 2024 22:47:54 +0100 Subject: [PATCH] tvs structure (#1300) Co-authored-by: Reynald Affeldt Co-authored-by: Cyril Cohen Co-authored-by: Zachary Stone --- CHANGELOG_UNRELEASED.md | 22 ++ _CoqProject | 1 + theories/Make | 1 + theories/charge.v | 2 +- theories/derive.v | 11 +- theories/exp.v | 4 +- theories/ftc.v | 19 +- theories/lebesgue_integral.v | 6 +- theories/lebesgue_measure.v | 6 +- theories/normedtype.v | 109 ++++++++-- theories/realfun.v | 4 +- theories/sequences.v | 6 +- theories/tvs.v | 402 +++++++++++++++++++++++++++++++++++ 13 files changed, 551 insertions(+), 42 deletions(-) create mode 100644 theories/tvs.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a191ece6d..312bf7076 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: diff --git a/_CoqProject b/_CoqProject index e36c71dae..ed73bd01a 100644 --- a/_CoqProject +++ b/_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 diff --git a/theories/Make b/theories/Make index 0d77fa421..eaefdc810 100644 --- a/theories/Make +++ b/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 diff --git a/theories/charge.v b/theories/charge.v index 498cc2228..d3329dce9 100644 --- a/theories/charge.v +++ b/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. diff --git a/theories/derive.v b/theories/derive.v index 2cd1198f7..da703d8d1 100644 --- a/theories/derive.v +++ b/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)); diff --git a/theories/exp.v b/theories/exp.v index 2e2d30497..cb7d2b8b7 100644 --- a/theories/exp.v +++ b/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 /=. diff --git a/theories/ftc.v b/theories/ftc.v index 7be07799d..bbc908701 100644 --- a/theories/ftc.v +++ b/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 []. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index b043af47c..5b2df0336 100644 --- a/theories/lebesgue_integral.v +++ b/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]. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e658b9a26..5fbc202ca 100644 --- a/theories/lebesgue_measure.v +++ b/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. diff --git a/theories/normedtype.v b/theories/normedtype.v index 8d0fc8437..839e7edbc 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -6,7 +6,8 @@ From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval ereal reals. From mathcomp Require Import signed topology prodnormedzmodule function_spaces. -From mathcomp Require Export real_interval separation_axioms. +From mathcomp Require Export real_interval separation_axioms tvs. + (**md**************************************************************************) (* # Norm-related Notions *) @@ -804,28 +805,110 @@ 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}. + +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 |; +}. -Section regular_topology. +HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. + +(* NB: These lemmas are done later with more machinery. They should + 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 /=. +exists (ball x (e / 2), ball y (e / 2)) => /=. + by split; apply: nbhsx_ballx; rewrite divr_gt0. +rewrite -ball_normE /ball_/= => xy /= [nx ny]. +by rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (splitr 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 /=. +near +oo_K => M. +pose r := `|e| / 2 / M. +exists (ball k r, ball x r). + by split; apply: nbhsx_ballx; rewrite !divr_gt0// normr_gt0// gt_eqF. +rewrite -ball_normE /ball/= => lz /= [nk nx]. +have := @ball_split _ _ (k *: lz.2) (k *: x) (lz.1 *: lz.2) `|e|. +rewrite -ball_normE /= real_lter_normr ?gtr0_real//. +rewrite (_ : _ < - e = false) ?orbF; last by rewrite ltr_nnorml// oppr_le0 ltW. +apply. + rewrite -scalerBr normrZ -(@ltr_pM2r _ M^-1) ?invr_gt0//. + by rewrite (le_lt_trans _ nx)// mulrC ler_pdivrMl// ler_wpM2r// invr_gt0. +rewrite -scalerBl normrZ. +rewrite (@le_lt_trans _ _ (`|k - lz.1| * M)) ?ler_wpM2l -?ltr_pdivlMr//. +rewrite (@le_trans _ _ (`|lz.2| + `|x|)) ?lerDl//. +rewrite (@le_trans _ _ (`|x| + (`|x| + r)))//. + rewrite addrC lerD// -lerBlDl -(normrN x) (le_trans (lerB_normD _ _))//. + by rewrite distrC ltW. +rewrite [leRHS](_ : _ = M^-1 * (M * M)); last first. + by rewrite mulrA mulVf ?mul1r// gt_eqF. +rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first. + by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA. +by rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl. +Unshelve. all: by end_near. Qed. -Variable R : numFieldType. +Lemma locally_convex : + exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. +Proof. +exists [set B | exists x 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. + rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first. + by rewrite opprD addrACA -scalerBr -scalerBr. + 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//. + by rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?gt_eqF. + by rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE ?gt_eqF. + have -> : `|1 - l| = 1 - `| l |. + by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->. + by rewrite -mulrDl addrCA subrr addr0 mul1r. +split. + move=> B [x] [r] ->. + rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE. + exists (r - `|x - y|) => /=; first by rewrite subr_gt0. + move=> z; rewrite -ball_normE/= ltrBrDr. + by apply: le_lt_trans; rewrite [in leRHS]addrC ler_distD. +move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. +by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. +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 standard_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. +End standard_topology. Lemma ball_itv {R : realFieldType} (x r : R) : ball x r = `]x - r, x + r[%classic. @@ -2301,14 +2384,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. diff --git a/theories/realfun.v b/theories/realfun.v index 70fae9c30..b11415d1c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1,12 +1,12 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality ereal reals signed. -From mathcomp Require Import topology prodnormedzmodule normedtype derive. +From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. From mathcomp Require Import sequences real_interval. -From HB Require Import structures. (**md**************************************************************************) (* # Real-valued functions over reals *) diff --git a/theories/sequences.v b/theories/sequences.v index bbff8a624..1e803af79 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -3,8 +3,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import set_interval. -From mathcomp Require Import reals ereal signed topology normedtype landau. +From mathcomp Require Import set_interval reals ereal signed topology. +From mathcomp Require Import tvs normedtype landau. (**md**************************************************************************) (* # Definitions and lemmas about sequences *) @@ -1123,7 +1123,7 @@ move=> k0 kfK; have [K0|K0] := lerP K 0. near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. by rewrite normr_gt0 t0 (lt_trans tk2) // -[in ltLHS](add0r k) midf_lt. -- apply/(@eqolim0 _ _ R (0^'))/eqoP => _/posnumP[e]; near=> x. +- apply/(@eqolim0 _ _ R 0^')/eqoP => _/posnumP[e]; near=> x. rewrite (le_trans (kfK _ _)) //=. + near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. diff --git a/theories/tvs.v b/theories/tvs.v new file mode 100644 index 000000000..564e20036 --- /dev/null +++ b/theories/tvs.v @@ -0,0 +1,402 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. +From mathcomp Require Import rat interval zmodp vector fieldext falgebra. +From mathcomp Require Import archimedean. +From mathcomp Require Import boolp classical_sets functions cardinality. +From mathcomp Require Import set_interval ereal reals signed topology. +From mathcomp Require Import prodnormedzmodule function_spaces. +From mathcomp Require Import separation_axioms. + +(**md**************************************************************************) +(* # Topological vector spaces *) +(* *) +(* This file introduces locally convex topological vector spaces. *) +(* ``` *) +(* tvsType R == interface type for a locally convex topological *) +(* vector space on a numDomain R *) +(* A tvs is constructed over a uniform space *) +(* TopologicalLmod_isTvs == factory allowing the construction of a tvs from *) +(* a lmodule which is also a topological space. *) +(* ``` *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +(* HB.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. *) +(* HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. *) +(* HB.structure Definition PointedLmodule (K : numDomainType) := *) +(* {M of Pointed M & GRing.Lmodule K M}. *) + +(* HB.structure Definition FilteredNmodule := {M of Filtered M M & GRing.Nmodule M}. *) +(* HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. *) +(* HB.structure Definition FilteredLmodule (K : numDomainType) := *) +(* {M of Filtered M M & GRing.Lmodule K M}. *) +HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. +HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. +HB.structure Definition NbhsLmodule (K : numDomainType) := + {M of Nbhs M & GRing.Lmodule K M}. + +HB.structure Definition TopologicalNmodule := {M of Topological M & GRing.Nmodule M}. +HB.structure Definition TopologicalZmodule := + {M of Topological M & GRing.Zmodule M}. +HB.structure Definition TopologicalLmodule (K : numDomainType) := + {M of Topological M & GRing.Lmodule K M}. +HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. +HB.structure Definition UniformLmodule (K : numDomainType) := + {M of Uniform M & GRing.Lmodule K M}. + +Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := + forall x y (lambda : R), x \in A -> y \in A -> + (0< lambda) -> (lambda < 1) -> lambda *: x + (1 - lambda) *: y \in A. + + +HB.mixin Record Uniform_isTvs (R : numDomainType) E + of Uniform E & GRing.Lmodule R E := { + add_continuous : continuous (fun x : E * E => x.1 + x.2) ; + scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; + locally_convex : exists2 B : set (set E), + (forall b, b \in B -> convex b) & basis B +}. + +#[short(type="tvsType")] +HB.structure Definition Tvs (R : numDomainType) := + {E of Uniform_isTvs R E & Uniform E & GRing.Lmodule R E}. + +Section properties_of_topologicallmodule. +Context (R : numDomainType) (E : topologicalType) + (Me : GRing.Lmodule R E) (U : set E). +Let ME := GRing.Lmodule.Pack Me. + +Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: (z.2 : ME))) (x : E) : + nbhs x U -> nbhs (-(x:ME)) (-%R @` (U : set ME)). +Proof. +move=> Ux; move: (f (-1, - (x:ME)) U); rewrite /= scaleN1r opprK => /(_ Ux) [] /=. +move=> [B] B12 [B1 B2] BU; near=> y; exists (- (y:ME)); rewrite ?opprK// -scaleN1r//. +apply: (BU (-1, y)); split => /=; last by near: y. +by move: B1 => [] ? ?; apply => /=; rewrite subrr normr0. +Unshelve. all: by end_near. Qed. + +Lemma nbhs0N_subproof (f : continuous (fun z : R^o * E => z.1 *: (z.2:ME) : E)) : + nbhs (0 :ME) (U : set ME) -> nbhs (0 : ME) (-%R @` (U : set ME)). +Proof. by move => Ux; rewrite -oppr0; exact: nbhsN_subproof. Qed. + +Lemma nbhsT_subproof (f : continuous (fun x : E * E => (x.1 : ME) + (x.2 : ME))) (x : E) : + nbhs (0 : ME) U -> nbhs (x : ME) (+%R (x : ME) @` U). +Proof. +move => U0; have /= := f (x, -(x : ME)) U; rewrite subrr => /(_ U0). +move=> [B] [B1 B2] BU; near=> x0. +exists ((x0 : ME) - (x : ME)); last by rewrite addrCA subrr addr0. +by apply: (BU ((x0 : ME), -(x : ME))); split; [near: x0; rewrite nearE|exact: nbhs_singleton]. +Unshelve. all: by end_near. Qed. + +Lemma nbhsB_subproof (f : continuous (fun x : E * E => (x.1 : ME) + (x.2 : ME))) (z x : E) : + nbhs (z : ME) U -> nbhs ((x : ME) + (z : ME)) (+%R (x : ME) @` U). +Proof. +move=> U0; move: (@f ((x : ME) + (z : ME), -(x : ME)) U); rewrite /= addrAC subrr add0r. +move=> /(_ U0)[B] [B1 B2] BU; near=> x0. +exists ((x0 : ME) - (x : ME)); last by rewrite addrCA subrr addr0. +by apply: (BU ((x0 : ME), -(x : ME))); split; [near: x0; rewrite nearE|exact: nbhs_singleton]. +Unshelve. all: by end_near. Qed. + +End properties_of_topologicallmodule. + +HB.factory Record TopologicalLmod_isTvs (R : numDomainType) E + of Topological E & GRing.Lmodule R E := { + add_continuous : continuous (fun x : E * E => x.1 + x.2) ; + scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; + locally_convex : exists2 B : set (set E), + (forall b, b \in B -> convex b) & basis B + }. + +HB.builders Context R E of TopologicalLmod_isTvs R E. + +Definition entourage : set_system (E * E) := + fun P => exists (U : set E), nbhs (0 : E) U /\ + (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). + +Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U). +Proof. by apply: nbhs0N_subproof; exact: scale_continuous. Qed. + +Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U). +Proof. +by apply: nbhsN_subproof; exact: scale_continuous. +Qed. + +Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). +Proof. by apply: nbhsT_subproof; exact: add_continuous. Qed. + +Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U). +Proof. by apply: nbhsB_subproof; exact: add_continuous. Qed. + +Lemma entourage_filter : Filter entourage. +Proof. +split; first by exists [set: E]; split => //; exact: filter_nbhsT. +- move=> P Q; rewrite /entourage nbhsE //=. + move=> [U [[B B0] BU Bxy]] [V [[C C0] CV Cxy]]. + exists (U `&` V); split. + by exists (B `&` C); [exact: open_nbhsI|exact: setISS]. + move=> xy; rewrite !in_setI => /andP[xyU xyV]. + by apply/andP;split; [exact: Bxy|exact: Cxy]. +- move=> P Q PQ; rewrite /entourage /= => [[U [HU Hxy]]]; exists U; split=> //. + by move => xy /Hxy /[!inE] /PQ. +Qed. + +Local Lemma entourage_refl (A : set (E * E)) : + entourage A -> [set xy | xy.1 = xy.2] `<=` A. +Proof. +rewrite /entourage => -[/= U [U0 Uxy]] xy /eqP; rewrite -subr_eq0 => /eqP xyE. +by apply/set_mem/Uxy; rewrite xyE; apply/mem_set; exact: nbhs_singleton. +Qed. + +Local Lemma entourage_inv : + forall A : set (E * E), entourage A -> entourage A^-1%relation. +Proof. +move=> A [/= U [U0 Uxy]]; rewrite /entourage /=. +exists (-%R @` U); split; first exact: nbhs0N. +move=> xy /set_mem /=; rewrite -opprB => [[yx] Uyx] /oppr_inj yxE. +by apply/Uxy/mem_set; rewrite /= -yxE. +Qed. + +Local Lemma entourage_split_ex (A : set (E * E)) : entourage A -> + exists2 B : set (E * E), entourage B & (B \; B)%relation `<=` A. +Proof. +move=> [/= U] [U0 Uxy]; rewrite /entourage /=. +have := @add_continuous (0, 0); rewrite /continuous_at/= addr0 => /(_ U U0)[]/=. +move=> [W1 W2] []; rewrite nbhsE/= => [[U1 nU1 UW1] [U2 nU2 UW2]] Wadd. +exists [set w | (W1 `&` W2) (w.1 - w.2)]. + exists (W1 `&` W2); split; last by []. + exists (U1 `&` U2); first exact: open_nbhsI. + by move=> t [U1t U2t]; split; [exact: UW1|exact: UW2]. +move => xy /= [z [H1 _] [_ H2]]; apply/set_mem/(Uxy xy)/mem_set. +rewrite [_ - _](_ : _ = (xy.1 - z) + (z - xy.2)); last by rewrite addrA subrK. +exact: (Wadd (xy.1 - z,z - xy.2)). +Qed. + +Local Lemma nbhsE : nbhs = nbhs_ entourage. +Proof. +have lem : -1 != 0 :> R by rewrite oppr_eq0 oner_eq0. +rewrite /nbhs_ /=; apply/funext => x; rewrite /filter_from/=. +apply/funext => U; apply/propext => /=; rewrite /entourage /=; split. +- pose V : set E := [set v | x - v \in U]. + move=> nU; exists [set xy | xy.1 - xy.2 \in V]; last first. + by move=> y /xsectionP; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE. + exists V; split => /=; last first. + by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE. + have /= := nbhsB x (nbhsN nU); rewrite subrr /= /V. + rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U])//. + apply/funext => /= v /=; rewrite inE; apply/propext; split. + by move=> [x0 [x1]] Ux1 <- <-; rewrite opprB addrCA subrr addr0. + move=> Uxy; exists (v - x); last by rewrite addrCA subrr addr0. + by exists (x - v) => //; rewrite opprB. +- move=> [A [U0 [nU UA]] H]; near=> z; apply: H; apply/xsectionP/set_mem/UA. + near: z; rewrite nearE; have := nbhsT x (nbhs0N nU). + rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U0])//. + apply/funext => /= z /=; apply/propext; split. + move=> [x0] [x1 Ux1 <-] <-; rewrite -opprB addrAC subrr add0r inE opprK//. + rewrite inE => Uxz; exists (z - x); last by rewrite addrCA subrr addr0. + by exists (x - z); rewrite ?opprB. +Unshelve. all: by end_near. Qed. + +HB.instance Definition _ := Nbhs_isUniform_mixin.Build E + entourage_filter entourage_refl + entourage_inv entourage_split_ex + nbhsE. +HB.end. + +Section Tvs_numDomain. +Context (R : numDomainType) (E : tvsType R) (U : set E). + +Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). +Proof. exact/nbhs0N_subproof/scale_continuous. Qed. + +Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). +Proof. exact/nbhsT_subproof/add_continuous. Qed. + +Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). +Proof. exact/nbhsB_subproof/add_continuous. Qed. + +End Tvs_numDomain. + +Section Tvs_numField. + +Lemma nbhs0Z (R : numFieldType) (E : tvsType R) (U : set E) (r : R) : + r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U). +Proof. +move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. +rewrite scaler0 => /(_ U0)[]/= B [B1 B2] BU. +near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r. +by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x]. +Unshelve. all: by end_near. Qed. + +Lemma nbhsZ (R : numFieldType) (E : tvsType R) (U : set E) (r : R) (x :E) : + r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U). +Proof. +move => r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U. +rewrite scalerA mulVf// scale1r =>/(_ U0)[] /= B [B1 B2] BU. +near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. +by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. +Unshelve. all: by end_near. Qed. + +End Tvs_numField. + +Section standard_topology. +Variable R : numFieldType. + +Lemma standard_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). +Proof. +(* NB(rei): almost the same code as in normedtype.v *) +move=> [/= x y]; apply/cvg_ballP => e e0 /=. +exists (ball x (e / 2), ball y (e / 2)) => /=. + by split; apply: nbhsx_ballx; rewrite divr_gt0. +rewrite /ball /ball_/= => xy /= [nx ny]. +by rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (splitr e) ltrD. +Qed. + +Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2). +Proof. +(* NB: This lemma is proved once again in normedtype, in a shorter way with much more machinery *) +(* To be rewritten once normedtype is split and tvs can depend on these lemmas *) +move=> [k x]; apply/cvg_ballP => e le0 /=. +pose M : R := maxr (`|e| + 1) (maxr `|k| (`|x| + `|x| + 2^-1 + 1)). +have M0l : 0 < `|e| + 1 by rewrite ltr_wpDl. +have M0r : 0 < maxr `|k| (`|x| + `|x| + 2^-1 + 1). + rewrite /maxr; case: ifPn => //. + have [->|k0 _] := eqVneq k 0; last by rewrite normr_gt0. + rewrite normr0 -ltrBlDr sub0r ltxx => /negbTE <-. + by rewrite (lt_le_trans (@ltrN10 _)). +have M0 : 0 < M. + by have /= -> := num_lt_max 0 (PosNum M0l) (PosNum M0r); rewrite M0l. +have Me : `|e| < M. + rewrite (@lt_le_trans _ _ (`|e| + 1)) ?ltrDl//. + have /= -> := num_le_max (`|e| + 1) (PosNum M0l) (PosNum M0r). + by rewrite lexx. +pose r := `|e| / 2 / M. +exists (ball k r, ball x r). + by split; exists r => //=; rewrite !divr_gt0// normr_gt0 gt_eqF. +move=> /= [z1 z2] [k1r k2r]. +have := @ball_split _ _ (k * z2) (k * x) (z1 * z2) `|e|. +rewrite /ball /= /= real_lter_normr ?gtr0_real//. +rewrite (_ : _ < - e = false) ?orbF; last by rewrite ltr_nnorml// oppr_le0 ltW. +apply. + rewrite -mulrBr normrM (@le_lt_trans _ _ (M * `|x - z2|)) ?ler_wpM2r//. + have /= -> := num_le_max `|k| (PosNum M0l) (PosNum M0r). + by apply/orP; right; rewrite /maxr; case: ifPn => // /ltW. + by rewrite -ltr_pdivlMl ?(lt_le_trans k2r)// mulrC. +rewrite -mulrBl normrM (@le_lt_trans _ _ (`|k - z1| * M)) ?ler_wpM2l//. + rewrite (@le_trans _ _ (`|z2| + `|x|))// ?lerDl ?normr_ge0//. + have z2xe : `|z2| <= `|x| + r. + by rewrite -lerBlDl -(normrN x) (le_trans (lerB_normD _ _))// distrC ltW. + rewrite (@le_trans _ _ (`|x| + r + `|x|)) ?lerD// addrC. + rewrite [leRHS](_ : _ = M^-1 * (M * M)); last first. + by rewrite mulrA mulVf ?mul1r// gt_eqF. + rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first. + by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA. + rewrite ler_wpM2l// ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl//. + rewrite (@lt_le_trans _ _ (`|x| + `|x| + 2^-1 + 1)) //. + by rewrite ltrDl ltr01. + rewrite (num_le_max _ (PosNum M0l) (PosNum M0r))//=. + apply/orP; right; have [->|k0] := eqVneq k 0. + by rewrite normr0 comparable_le_max ?real_comparable// lexx orbT. + have nk0 : 0 < `|k| by rewrite normr_gt0. + have xx21 : 0 < `|x| + `|x| + 2^-1 + 1%R by rewrite addr_gt0. + by rewrite (num_le_max _ (PosNum nk0) (PosNum xx21))// lexx orbT. +by rewrite -ltr_pdivlMr ?(lt_le_trans k1r) ?normr_gt0. +Qed. + +Lemma standard_locally_convex : + exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B. +Proof. +(* NB(rei): almost the same code as in normedtype.v *) +exists [set B | exists x r, B = ball x r]. + move=> b; rewrite inE /= => [[x]] [r] -> z y l. + rewrite !inE /ball /= => zx yx l0; rewrite -subr_gt0 => l1. + have -> : x = l *: x + (1 - l) *: x. + by rewrite scalerBl addrCA subrr addr0 scale1r. + rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first. + by rewrite opprD addrACA -mulrBr -mulrBr. + rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//. + by rewrite -!normrM ler_normD. + rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//. + rewrite ltr_leD//. + by rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?gt_eqF. + by rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE ?gt_eqF. + have -> : `|1 - l| = 1 - `| l |. + by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->. + by rewrite -mulrDl addrCA subrr addr0 mul1r. +split. + move=> B [x] [r] ->. + rewrite openE/= /ball/= /interior => y /= bxy; rewrite -nbhs_ballE. + exists (r - `|x - y|) => /=; first by rewrite subr_gt0. + move=> z; rewrite /ball/= ltrBrDr. + by apply: le_lt_trans; rewrite [in leRHS]addrC ler_distD. +move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. +by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. +Qed. + +HB.instance Definition _ := Uniform_isTvs.Build R (R^o)%type + standard_add_continuous standard_scale_continuous standard_locally_convex. + +End standard_topology. + +Section prod_Tvs. +Context (K : numFieldType) (E F : tvsType K). + +Lemma prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2). +Proof. +move => [/= xy1 xy2] /= U /= [] [A B] /= [nA nB] nU. +have [/= A0 [A01 A02] nA1] := @add_continuous K E (xy1.1, xy2.1) _ nA. +have [/= B0 [B01 B02] nB1] := @add_continuous K F (xy1.2, xy2.2) _ nB. +exists ([set xy | A0.1 xy.1 /\ B0.1 xy.2], [set xy | A0.2 xy.1 /\ B0.2 xy.2]). + by split; [exists (A0.1, B0.1)|exists (A0.2, B0.2)]. +move => [[x1 y1][x2 y2]] /= [] [] a1 b1 [] a2 b2. +by apply: nU; split; [exact: (nA1 (x1, x2))|exact: (nB1 (y1, y2))]. +Qed. + +Lemma prod_scale_continuous : continuous (fun z : K^o * (E * F) => z.1 *: z.2). +Proof. +move => [/= r [x y]] /= U /= []/= [A B] /= [nA nB] nU. +have [/= A0 [A01 A02] nA1] := @scale_continuous K E (r, x) _ nA. +have [/= B0 [B01 B02] nB1] := @scale_continuous K F (r, y) _ nB . +exists (A0.1 `&` B0.1, A0.2 `*` B0.2). + by split; [exact: filterI|exists (A0.2,B0.2)]. +by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split; + [exact: (nA1 (l, e))|exact: (nB1 (l, f))]. +Qed. + +Lemma prod_locally_convex : + exists2 B : set (set (E * F)), (forall b, b \in B -> convex b) & basis B. +Proof. +have [Be Bcb Beb] := @locally_convex K E. +have [Bf Bcf Bfb] := @locally_convex K F. +pose B := [set ef : set (E * F) | open ef /\ + exists be, exists2 bf, Be be & Bf bf /\ be `*` bf = ef]. +have : basis B. + rewrite /basis/=; split; first by move=> b => [] []. + move=> /= [x y] ef [[ne nf]] /= [Ne Nf] Nef. + case: Beb => Beo /(_ x ne Ne) /= -[a] [] Bea ax ea. + case: Bfb => Bfo /(_ y nf Nf) /= -[b] [] Beb yb fb. + exists [set z | a z.1 /\ b z.2]; last first. + by apply: subset_trans Nef => -[zx zy] /= [] /ea + /fb. + split=> //=; split; last by exists a, b. + rewrite openE => [[z z'] /= [az bz]]; exists (a, b) => /=; last by []. + rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo. + by exists b => //; split => // []; exact: Bfo. +exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-. +move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1. +by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE]. +Qed. + +HB.instance Definition _ := + Uniform_isTvs.Build K (E * F)%type + prod_add_continuous prod_scale_continuous prod_locally_convex. + +End prod_Tvs.