From 1d17335bc1835381c099d9c642d6e5d58fc7c430 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Fri, 20 Mar 2026 11:14:19 +0900 Subject: [PATCH 1/3] adding seminorms to tvs - adding also initial fam topology, gauge functions, and subbase 0basis - hahn banach initial_subctvs Co-authored-by: Reynald Affeldt Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 71 + classical/classical_sets.v | 44 + classical/unstable.v | 15 + theories/convex.v | 35 + .../functional_analysis/hahn_banach_theorem.v | 110 +- theories/normedtype_theory/normed_module.v | 26 +- .../pseudometric_normed_Zmodule.v | 33 +- theories/normedtype_theory/tvs.v | 1360 +++++++++++++++-- theories/topology_theory/initial_topology.v | 8 +- theories/topology_theory/topology_structure.v | 15 +- 10 files changed, 1535 insertions(+), 182 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6e327b2b46..f30ec429b2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -49,6 +49,7 @@ + lemma `initial_unif_continuous_comp` + lemma `initial_unif_continuous_comp_fst` + lemma `initial_unif_continuous_comp_snd` + + lemma `initial_nbhs_preimage` - in `product_topology.v`: + lemma `entourage_prod_exS` @@ -81,6 +82,69 @@ + definitions `clamp`, `clamp_gele` + lemmas `clamp_gemin`, `clamp_lemax`, `minmax_clamp`, `clamp_id`, `clamp_min`, `clamp_max` + + lemma `seminorm_normrB` + +- in `topology_structure.v`: + + lemma `id_continuous` + + definition `nbhs_basis` + + definition `openU_from` + +- in `normed_module.v`: + + lemma `ball_convex_set` (was a `Let`) + +- in `classical_sets.v`: + + notation ``... `+ ...`` + + lemmas `addsetS`, `add0set`, `addsetI`, `addsetA` + +- in `convex.v`: + + lemmas `lt_conv`, `le_conv` + + lemma `convD` + +- in `pseudmetric_normed_Zmodule.v`: + + lemma `continuous_shift` + + lemma `nbhs_add1set` + +- in `tvs.v`: + + definition `balanced_set` + + definition `absolutely_convex_set` + + lemma `absolutely_convex0` + + definition `absorbing_set` + + lemma `absolutely_convex_setX` + + definition `init_subconvextvs` + + factory `NbhsBasisAt0_isConvexTvs` + + definition `filter_from_basis0` + + factory `NbhsSubbasisAt0_isConvexTvs` + + definition `finI_fromsubbasis0` + + lemma `openD` + + lemma `openB` + + lemma `nbhsE0` + + lemma `openZ` + + lemma `scalerx_continuous` + + lemma `scalexr_continuous` + + definition `nbhsbasis_convextvs` + + definition `open_nbhsbasis_convextvs` + + definition `open_absconvex_opennbhsbasis` + + definition `basis_opennbhsbasis` + + lemma `basis_neqset0` + + lemma `absorbing_opennbhsbasis` + + definition `gauge_fun` + + definition `seminorm_on` + + definition `seminorm_subbasis` + + lemmas `nonempty_subbasis`, `mem0_seminorm_subbasis`, `split_seminorm_subbasis`, + `expand_seminorm_subbasis` + + lemmas `convex_seminorm_subbasis`, `balanced_seminorm_subbasis`, + `absolutely_convex_seminorm_subbasis`, `absorbing_seminorm`, `continuous_at0_seminorm`, + `continuous_seminorm` + + definitions `gauge_fun_basis`, `seminorm_of` + + theorem `seminorm_convextvs` + + lemma `continuous_seminorm_of` + + lemma `linear_continuous_seminorm` + + lemma `linear_seminorm_continuous` + + proposition `lcfun_seminorm` + +- in `hahn_banach_theorem.v` + + theorem `hahn_banach_extension_subctvs` + + theorem `hahn_banach_extension_initialsubctvs` - in `sequences.v`, + lemmas `is_cvg_series_shiftn`, `near_series_squeeze_is_cvgn` @@ -223,6 +287,8 @@ - moved to `lebesgue_Rintegral.v` from `radon_nikodym.v` and renamed: + `semi_sigma_additive_nng_induced` -> `semi_sigma_additive_measure_of_density` +- in `tvs.v`: + + mixin `Uniform_isConvexTvs` (now uses `absolutely_convex_set` and `nbhs_basis 0`) ### Renamed @@ -237,6 +303,11 @@ - in `normed_module.v`: + `PseudoMetricNormedZmod_ConvexTvs_isNormedModule` -> `MetricNormedZmod_ConvexTvs_isNormedModule` +- in `tvs.v`: + + lemma `nbhsT_subproof` -> `nbhsD_subproof` + + lemma `nbhsT` -> `nbhsD0` + + lemma `nbhsB` -> `nbhsD` + - in `pseudometric_normed_Zmodule.v`: + `continuous_within_itvP` -> `continuous_within_itvccP` - in `radon_nikodym.v`: diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 3c421f419c..5ff1920889 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -117,6 +117,9 @@ From mathcomp Require Import boolp wochoice. (* X `x` Y := cross fst snd X Y *) (* ``` *) (* *) +(* ``A `+ B`` *) +(* : $\{ x + y | x\in A, x\in B\}$ *) +(* *) (* ``` *) (* *) (* R ^nat == notation for the type of sequences, i.e., *) @@ -280,6 +283,7 @@ Reserved Notation "F `#` G" (at level 48, left associativity, format "F `#` G"). Reserved Notation "'`I_' n" (at level 8, n at level 2, format "'`I_' n"). Reserved Notation "A `x` B" (at level 46, left associativity). +Reserved Notation "A `+ B" (at level 50). Definition set T := T -> Prop. (* we use fun x => instead of pred to prevent inE from working *) @@ -1740,6 +1744,46 @@ End cross. Definition cross12 {T1 T2 : Type} := @cross (T1 * T2)%type T1 T2 fst snd. Notation "A `x` B" := (cross12 A B) : classical_set_scope. +Notation "A `+ B" := [set (x + y)%R | x in A & y in B]. + +Section addsetTheory. +Context {E : zmodType}. +Import GRing.Theory. +Local Open Scope ring_scope. +Implicit Types A B C D : set E. + +Lemma addsetS A B C D : A `<=` B -> C `<=` D -> A `+ C `<=` B `+ D. +Proof. +by move=> AB CD z [a /AB Ba [c /CD Dc <-]]; exists a => //; exists c. +Qed. + +Lemma add0set A : [set 0] `+ A = A. +Proof. +apply/seteqP; split => z /=. + by move=> [+ -> [y]]; rewrite add0r => + + <-. +by move=> Az; exists 0 => //; exists z; rewrite ?add0r. +Qed. + +Lemma addsetI A B (x : E) : + [set x] `+ (A `&` B) = ([set x] `+ A) `&` ([set x] `+ B). +Proof. +apply/seteqP; split => z. + by move => [r Cr] [y [Ay By] <- {z}]; split => /=; exists r => //; + exists y. +move=> /= [[r ->] [y Ay] <- {z}] [x' ->] [y' By'] /(congr1 (fun h => h - x)). +rewrite addrAC subrr add0r addrAC subrr add0r => yy'. +move: By'; rewrite yy' {y' yy'} => By. +by exists x => //; exists y. +Qed. + +Lemma addsetA x y A : [set x + y] `+ A `<=` [set x] `+ ([set y] `+ A). +Proof. +move=> _/= [_ ->] [z Az <-]; exists x => //; exists (y + z); last exact: addrA. +by exists y => //; exists z. +Qed. + +End addsetTheory. + Lemma subKimage {T T'} {P : set_system T'} (f : T -> T') (g : T' -> T) : cancel f g -> [set A | P (f @` A)] `<=` [set g @` A | A in P]. Proof. by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed. diff --git a/classical/unstable.v b/classical/unstable.v index f3ff7f79b3..71c1db4983 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -680,6 +680,21 @@ by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD. Qed. End Theory. + +Section realTheory. +Variables (K : realDomainType) (L : lmodType K) (norm : SemiNorm.type L). + +Lemma seminorm_normrB x y: `|norm x - norm y| <= norm (x - y). +Proof. +have [pxy | pyx] := leP (norm x) (norm y). + rewrite ler0_norm ?subr_le0 // opprB. + rewrite lerBlDl; rewrite -(@normN _ _ norm (x-y)) opprB. + by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +rewrite gtr0_norm ?subr_gt0 // lerBlDl. +by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK. +Qed. + +End realTheory. End Theory. Module Import Exports. HB.reexport. End Exports. diff --git a/theories/convex.v b/theories/convex.v index 89dccb9c51..52290486c4 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -49,6 +49,32 @@ Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +Lemma lt_conv {R : realFieldType} (x y r e : R) : + 0 <= r -> r <= 1 -> x < e -> y < e -> r * x + r.~ * y < e. +Proof. +move => r0 r1 xe ye. +have [->|] := eqVneq r 0; first by rewrite mul0r /onem subr0 add0r mul1r. +have [->|] := eqVneq r 1; first by rewrite mul1r /onem subrr mul0r addr0. +move=> rneq0 rneq1. +have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. +apply: ltrD. +rewrite lter_pM2l lt_neqAle; apply/andP; split => //; first by rewrite eq_sym. +by move: xe; rewrite lt_def; move/andP => []; rewrite eq_sym //. +by apply: ltW. +rewrite lter_pM2l /onem ?subr_gt0 ?ltW //. +by rewrite lt_def; apply/andP; split => //; rewrite eq_sym. +Qed. + +Lemma le_conv {R : realFieldType} (x y r e : R): + 0 <= r -> r <= 1 -> 0 <= x -> x <= e -> 0 <= y -> y <= e -> r * x + r.~ * y <= e. +Proof. +move => r0 r1 x0 xe y0 ye. +rewrite /onem. +have -> : e = r * e + (1 -r) * e by rewrite -mulrDl addrCA subrr addr0 mul1r. +apply: lerD; first by rewrite ler_pM. +by rewrite ler_pM ?subr_ge0 //. +Qed. + Declare Scope convex_scope. Local Open Scope convex_scope. @@ -163,6 +189,15 @@ HB.instance Definition _ := End lmodType_convex_space. +Lemma convD (R : numDomainType) (E : lmodType R) (t : {i01 R}) (x y z' : convex_lmodType E) : + x <| t |> y + z' = (x + z' : convex_lmodType _) <| t |> (y + z'). +Proof. +rewrite /conv/=. +rewrite !scalerDr -[in RHS]addrA. +rewrite [in X in (_ = _ + X)]addrCA [in X in (_ = _ + ( _ + X))]scalerBl. +by rewrite [in X in (_ = _ + ( _ + X))]addrCA addrN addr0 scale1r addrA. +Qed. + Definition convex_numDomainType (R : numDomainType) : Type := R^o. Section numDomainType_convex_space. diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index c29a495541..378d8e7bc3 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -14,11 +14,21 @@ From mathcomp Require Import reals convex topology normedtype. (* convex function, can be extended to a linear map on V bounded by the same *) (* convex function. *) (* Theorem `hahn_banach_extension_normed` specifies this to the extension of *) -(* a linear continuous function on a subspace to the whole normed module. *) +(* a linear continuous function defined on a subnormedmodule to the whole *) +(* normed module. *) +(* Theorem `hahn_banach_extension_subctvs` allows to extend a linear function *) +(* defined on a subconvextvs to a convextvs. *) +(* Theorem `hahn_banach_extension_initialsubctvs` allows to extend a linear *) +(* function defined on a sublmodule to a convextvs. *) (* *) +(* | Extension theorem | subcodomain | codomain |*) +(* |--------------------------------------|------------------|---------------|*) +(* | hahn_banach_extension | subLmodType | lmodType |*) +(* | hahn_banach_extension_normed | subNormedmodType | normedModType |*) +(* | hahn_banach_extension_subcvts | subconvextvsType | convexTvsType |*) +(* | hahn_banach_extension_initialsubctvs | subLmodType | convexTvsType |*) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -31,7 +41,6 @@ Local Open Scope ring_scope. Local Open Scope convex_scope. Local Open Scope real_scope. -(* TODO : use a lightweight factory to make every subLmodType a subnormedmodtype *) (**md module with definitions on linear relations, thought of as graph of functions *) @@ -67,8 +76,8 @@ End LinearGraphInternal. Module HahnBanachZornInternal. Section hahnbanachzorn. Import LinearGraphInternal. -Context (R : realType) (V : lmodType R) (F : pred V). -Variables (F' : subLmodType F) (phi : {linear F' -> R}) (p : V -> R). +Context (R : realType) (V : lmodType R) (F : pred V) + (F' : subLmodType F) (phi : {linear F' -> R}) (p : V -> R). Implicit Types f g : graph V. @@ -357,3 +366,94 @@ by exists g'. Qed. End hahn_banach_normed. + +Section hahn_banach_extension_ctvs. +Context {R : realType} {V : convexTvsType R} (F : pred V). +(**md Contrary to the normed case, the extension theorem is not true for any + subtopology on `F`, but only for the finest one. *) + +Import Norm. + +(** A first version specifying the seminorm bounding the function *) +(**md [Jarchow 7.1.2] +Let $V$ be a real vector space, $F$ a subspace of $V$, and $p \in V^{\#}$ +(the set of all sublinear functionals on $V$) and $p$ is a seminorm, +if $f \in F^*$ satisfies $|f| \leq p|_F$, then a $g\in V^*$ exists +such that $g|_F = f$. *) +Theorem hahn_banach_extension_subctvs (F' : subConvexTvsType F) + (f : {linear F' -> R}) : + (exists2 p : SemiNorm.type V, + seminorm_of p & forall z : F', f z <= p (val z)) -> + exists g : {linear_continuous V -> R}, forall x : F', g (val x) = f x. +Proof. +move=> [p ps fp]. +have convp : @convex_function _ _ [set: V] p. + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /= (le_trans (ler_normD _ _))//. + rewrite !normZ (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~)//. + exact: onem_ge0. +have [g majgp F_eqgf] := @hahn_banach_extension R V _ F' f p convp fp. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + by apply/lcfun_seminorm; exists p => //; exact: continuous_seminorm_of. +pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. +by exists g'. +Qed. + +(**md A second version where `F` is a subspace of `V`, meaning endowed with + the initial topology w.r.t. to `val`. *) +(**md [Jarchow, 7.2.1] Let $F$ be a subspace of the lcs $V$. Then every + continuous linear form $f:F\to \mathbb{K}$ extends to a continuous + linear form $g:V\to \mathbb{K}$. *) +Theorem hahn_banach_extension_initialsubctvs (F' : subLmodType F) + (f : {linear_continuous (init_subconvextvs F') -> R^o}) : + exists g : {linear_continuous V -> R}, forall x : F', g (val x) = f x. +Proof. +have [[openBasisV BasisV] _] := has_open_nbhs_basis V. +have [p' ps' fp'] : exists2 p : SemiNorm.type V, + seminorm_of p & forall z : F', f z <= p (val z). + have : continuous (f : init_subconvextvs F' -> R^o) by exact: continuous_fun. + move=> /linear_continuous_seminorm[p [cp ps] /= fp]. + have [/= nF [onF pF]] := cp. + have [/(_ nF onF) + _] := basis_opennbhsbasis (init_subconvextvs F'). + move=> [oF [[/= oV] ooV oVF] oF0 oFn]. + have /BasisV [/= bV obV boV] : nbhs 0 oV. + rewrite nbhsE; exists oV => //; split => //. + apply: (@image_preimage_subset _ _ (val : F'-> V)). + by rewrite oVF; exists 0; rewrite ?linear0. + exists (gauge_fun_basis obV); first by exists bV, obV. + move=> z. + set pVz := (leRHS). + apply: le_trans; first exact: fp. + rewrite pF; apply: inf_le. + - move=> x /= [r [r0]] /set_mem[v bVv rvalz] <-. + exists (- r); split => //; exists r; split => //. + rewrite inE; exists (r^-1 *: z). + apply: oFn; rewrite -oVF /=; apply: boV. + by rewrite linearZ/= -rvalz scalerA mulVf ?scale1r ?gt_eqF. + by rewrite scalerA divff ?scale1r ?gt_eqF. + - have [/= s s0 szbV]:= absorbing_opennbhsbasis obV (val z). + exists s^-1; split; rewrite ?invr_gt0// inE /=. + exists (s *: val z); first exact/set_mem. + by rewrite scalerA mulVf ?scale1r// gt_eqF. + - split; last by exists 0 => r [? _]; rewrite ltW. + have [/= s s0 sznF]:= absorbing_opennbhsbasis onF z. + exists s^-1; split; rewrite ?invr_gt0// inE /=. + exists (s *: z); first exact/set_mem. + by rewrite scalerA mulVf ?scale1r// gt_eqF. +(* apply the previous thm but typing or... *) +have convp : @convex_function _ _ [set: V] p'. + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /= (le_trans (ler_normD _ _))//. + by rewrite !normZ (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~)// onem_ge0. +have [g majgp F_eqgf] := @hahn_banach_extension R V _ F' f p' convp fp'. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + by apply/lcfun_seminorm; exists p' => //; exact: continuous_seminorm_of. +pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. +by exists g'. +Qed. + +End hahn_banach_extension_ctvs. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index d89a260072..bec9661095 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -136,7 +136,7 @@ Unshelve. all: by end_near. Qed. Local Open Scope convex_scope. -Let ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r). +Lemma ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r). Proof. apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. rewrite inE/=. @@ -149,16 +149,24 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl. by rewrite ltrD// ltr_pM2l// onem_gt0. Qed. +#[local] Lemma ball_balanced_set (r : K) : balanced_set (ball (0 : V) r). +Proof. +move=> t /= t1 z /= [y]. +rewrite -ball_normE /= !sub0r !normrN => + <-. +by rewrite normrZ; apply: le_lt_trans; rewrite ler_piMl. +Qed. + (** NB: we have almost the same proof in `tvs.v` *) Let locally_convex_set : exists2 B : set_system (convex_lmodType V), - (forall b, b \in B -> convex_set b) & basis B. + (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B. Proof. -exists [set B | exists (x : convex_lmodType V) r, B = ball x r]. - by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set. -split; first by move=> B [x] [r] ->; exact: ball_open. -move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. -by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. +exists [set B | exists2 r, 0 < r & B = ball 0 r]. + move=> b; rewrite inE /= => -[r _ ->]; split; first exact: ball_convex_set. + exact: ball_balanced_set. +split; first by move=> /= a [r r0 ->]; apply: nbhsx_ballx. +move=> /= b; rewrite -nbhs_ballE => -[r /= r0] b0r /=. +by exists (ball 0 r)=> //; exists r. Qed. (* NB: was needed until version 1.18.0 *) @@ -1995,10 +2003,6 @@ rewrite (le_lt_trans (fr r _ _))// -?ltr_pdivlMl//. by near: z; apply: cvgr_dist_lt => //; rewrite mulrC divr_gt0. Unshelve. all: by end_near. Qed. -Lemma continuousfor0_continuous (f : {linear V -> W}) : - {for 0, continuous f} -> continuous f. -Proof. by move=> /continuous_linear_bounded/bounded_linear_continuous. Qed. - Lemma linear_bounded_continuous (f : {linear V -> W}) : bounded_near f (nbhs 0) <-> continuous f. Proof. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index dc258fd1f1..eb070aab1b 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -136,7 +136,7 @@ HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. Section TopologicalNmodule_theory. -Context {E : topologicalType} {F : topologicalNmodType} (U : set_system E). +Context {E : Type} {F : topologicalNmodType} (U : set_system E). Lemma cvg_sum (I : Type) (r : seq I) (P : pred I) (Ff : I -> E -> F) (Fa : I -> F) : @@ -144,9 +144,21 @@ Lemma cvg_sum (I : Type) (r : seq I) (P : pred I) \sum_(i <- r | P i) Ff i x @[x --> U] --> \sum_(i <- r| P i) Fa i. Proof. by move=> FF Ffa; apply: cvg_big => //; exact: add_continuous. Qed. +Lemma continuous_shift (x y : F) : {for x, continuous (+%R^~ y)}. +Proof. +have -> : +%R^~ y = (fun z => z.1 + z.2) \o (fun z => (z, y)) by exact: funext. +apply: continuous_comp (@add_continuous _ (x, y)). +by apply: cvg_pair => //=; exact: cvg_cst. +Qed. + +End TopologicalNmodule_theory. + +Section TopologicalNmodule_theory. +Context {E : topologicalType} {F : topologicalNmodType}. + Lemma sum_continuous (I : Type) (r : seq I) (P : pred I) (f : I -> E -> F) : - (forall i : I, P i -> continuous (f i)) -> - continuous (fun x1 : E => \sum_(i <- r | P i) f i x1). + (forall i, P i -> continuous (f i)) -> + continuous (fun x => \sum_(i <- r | P i) f i x). Proof. by move=> FC0; apply: continuous_big => //; exact: add_continuous. Qed. End TopologicalNmodule_theory. @@ -234,6 +246,21 @@ Qed. Lemma nbhsB (U : set M) (z x : M) : nbhs z U -> nbhs (x + z) (+%R x @` U). Proof. exact/nbhsB_subproof/add_continuous. Qed. +Lemma nbhs_add1set x (A : set M) : nbhs 0 A <-> nbhs x ([set x] `+ A). +Proof. +split=> [|nx]. + rewrite -(subrr x) => /continuous_shift. + suff -> : [set x] `+ A = +%R^~ (- x) @^-1` A by []. + apply: funext => z /=; apply: propext; split => [|Azx]. + by move=> [? -> [y By] <-]; rewrite addrAC subrr add0r. + by exists x => //; exists (z - x) => //; rewrite addrCA subrr addr0. +suff -> : A = +%R^~ x @^-1` ([set x] `+ A). + by apply: continuous_shift; rewrite add0r. +apply: funext => z /=; apply: propext; split=> [Az|[_ -> [y By]]]. + by exists x => //; exists z => //; rewrite addrC. +by rewrite addrC => /addIr <-. +Qed. + End TopologicalZmoduleTheory. HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 10f64f9df3..8b3f88c1b5 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -1,61 +1,104 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum vector. -From mathcomp Require Import interval_inference. +From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import convex set_interval reals topology num_normedtype. +From mathcomp Require Import convex set_interval reals topology. +From mathcomp Require Import initial_topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. (**md**************************************************************************) (* # Topological vector spaces *) (* *) (* This file introduces locally convex topological vector spaces. *) -(* ``` *) -(* NbhsLmodule K == HB class, join of Nbhs and Lmodule over K *) -(* K is a numDomainType. *) -(* preTopologicalLmodType K == topological space and Lmodule over K *) -(* K is a numDomainType *) -(* The HB class is PreTopologicalLmodule. *) -(* topologicalLmodType K == topologicalNmodule and Lmodule over K with a *) -(* continuous scaling operation *) -(* The HB class is TopologicalLmodule. *) -(* convexTvsType R == interface type for a locally convex *) -(* tvs on a numDomain R *) -(* A convex tvs is constructed over a uniform *) -(* space. *) -(* The HB class is ConvexTvs. *) -(* subConvexTvsType R V S == join of subTopologicalType, convexTvsType, *) -(* and subLmoduleType *) -(* The HB class is SubConvexTvs. *) -(* Instance: in particular, it is shown that a *) -(* sub-Lmodule is a sub-convex TVS. *) -(* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a *) -(* convex tvs from an Lmodule which is also a *) -(* topological space *) -(* {linear_continuous E -> F} == the type of all linear and continuous *) -(* functions between E and F, where E is a *) -(* NbhsLmodule.type and F a NbhsZmodule.type over *) -(* a numDomainType R *) -(* The HB class is called LinearContinuous. *) -(* The notation {linear_continuous E -> F | s} *) -(* also exists. *) -(* lcfun E F s == membership predicate for linear continuous *) -(* functions of type E -> F with scalar operator *) -(* s : K -> F -> F *) -(* E and F have type convexTvsType K. *) -(* This is used in particular to attach a type of *) -(* lmodType to {linear_continuous E -> F | s}. *) -(* lcfun_spec f == specification for membership of the linear *) -(* continuous function f *) -(* ``` *) +(* *) +(* `balanced_set A` *) +(* : $\forall r, |r|\leq 1 \to rA \subseteq A$ *) +(* *) +(* `absolutely_convex_set A` *) +(* : convex and balanced set *) +(* *) +(* `absorbing_set A` *) +(* : $\forall x, \exists r, r>0 \land rx\in A$ *) +(* *) +(* `NbhsLmodule K` *) +(* : HB join of `Nbhs` and `Lmodule` over `K`, a `numDomainType` *) +(* *) +(* `preTopologicalLmodType K` *) +(* : topological space and `Lmodule` over `K`, a `numDomainType` *) +(* : The HB class is `PreTopologicalLmodule`. *) +(* *) +(* `topologicalLmodType K` *) +(* : `topologicalNmodule` and `Lmodule` on `K ` with a continuous scaling *) +(* : operation *) +(* : The HB class is `TopologicalLmodule`. *) +(* *) +(* `convexTvsType R` *) +(* : interface type for a locally convex TVS on a `numDomainType` `R` *) +(* : A convex TVS is constructed over a uniform space. *) +(* : The HB class is `ConvexTvs`. *) +(* *) +(* `subConvexTvsType R V S` *) +(* : join of `subTopologicalType`, `convexTvsType`, and `subLmoduleType` *) +(* : The HB class is `SubConvexTvs`. *) +(* : Instance: in particular, it is shown that a sub-Lmodule is a sub-convex *) +(* : TVS. *) +(* *) +(* `init_subconvextvs` *) +(* : the subConvexTvs structure on any subLmodule in a convexTvs, endowed *) +(* : with the initial topology induced by the embedding *) +(* *) +(* `PreTopologicalLmod_isConvexTvs` *) +(* : factory allowing the construction of a convex TVS from an Lmodule which *) +(* : is also a topological space *) +(* *) +(* `{linear_continuous E -> F}` *) +(* : the type of all linear and continuous functions between E and F, where E *) +(* : is a NbhsLmodule.type and F a NbhsZmodule.type over a numDomainType R *) +(* : The HB class is called LinearContinuous. *) +(* : The notation `{linear_continuous E -> F | s}` also exists. *) +(* *) +(* `lcfun E F s` *) +(* : membership predicate for linear continuous functions of type `E -> F` h *) +(* : with scalar operator `s : K -> F -> F` *) +(* : `E` and `F` have type `convexTvsType K`. *) +(* : This is used in particular to attach a type of `lmodType` to *) +(* : `{linear_continuous E -> F | s}`. *) +(* *) +(* `lcfun_spec f` *) +(* : specification for membership of the linear continuous function f *) +(* *) +(* `gauge_fun` *) +(* : Also called the Minkowski functional, the gauge function on an *) +(* : absolutely convex and absorbing subset is the distance of a point to *) +(* : this subset. It is endowed with a `Seminorm.type` structure. *) +(* *) +(* `seminorm_on` *) +(* : builds a `convexTvsType` structure on a `Lmodule` from a nonempty family *) +(* : of seminorms *) +(* *) +(* `seminorm_subbasis` *) +(* : the subbasis of neighbourhoods for `seminorm_on`, built as the reverse *) +(* : image by the seminorms of open balls centered at 0 *) +(* *) +(* `gauge_fun_basis` *) +(* : a gauge functional for an element of the basis of open neighbourhoods *) +(* : for a `convexTvsType` *) +(* *) +(* `seminorm_of` *) +(* : the family of gauge functionals for the basis of open neighbourhoods for *) +(* : a `convexTvsType`. It is shown to generate through seminorm_on the same *) +(* : topology as the one generated by the said basis. *) +(* *) (* HB instances: *) -(* - The type R^o (R : numFieldType) is endowed with the structure of *) -(* ConvexTvs. *) -(* - The product of two Tvs is endowed with the structure of ConvexTvs. *) -(* - {linear_continuous E-> F} is endowed with a lmodType structure when E *) -(* and F are convexTvs. *) +(* - The type `R^o` (`R : numFieldType`) is endowed with the structure of *) +(* `ConvexTvs`. *) +(* - The product of two TVS is endowed with the structure of `ConvexTvs`. *) +(* - `{linear_continuous E-> F}` is endowed with a lmodType structure when *) +(* `E` and `F` are `ConvexTvs`. *) +(* *) (******************************************************************************) Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'" @@ -65,7 +108,6 @@ Reserved Notation "'{' 'linear_continuous' U '->' V '}'" (at level 0, U at level 98, V at level 99, format "{ 'linear_continuous' U -> V }"). -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -76,6 +118,38 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +Section absolutely_convex. +Context {K : numDomainType} {V : lmodType K}. +Implicit Type A : set V. + +Definition balanced_set A := forall r, `|r| <= 1 -> ( *:%R r) @` A `<=` A. + +Definition absolutely_convex_set A := convex_set A /\ balanced_set A. + +Lemma absolutely_convex0 A : A !=set0 -> absolutely_convex_set A -> A 0. +Proof. +move => [] x Ax [] _ /(_ 0); rewrite normr0 ler01 // => /(_ isT) /(_ 0); apply. +by exists x; rewrite //= scale0r. +Qed. + +Definition absorbing_set A := forall x : V, exists2 r, 0 < r & r *: x \in A. + +End absolutely_convex. + +Lemma absolutely_convex_setX (K : numDomainType) (E F : lmodType K) + (A : set E) (B : set F) : + absolutely_convex_set A -> absolutely_convex_set B -> + absolutely_convex_set (A `*` B). +Proof. +move=> [convA balA] [convB balB]; split. +- move => [x1 y1] [x2 y2] l /[!inE] /= -[Ax1 By1] [Ax2 By2]; split. + + by apply/set_mem/convA; exact/mem_set. + + by apply/set_mem/convB; exact/mem_set. +- move=> r r1 [x1 y1] [[x2 y2]]/= [Ax2 By2] [] <- <-; split. + + by apply/balA; [exact: r1|exists x2]. + + by apply/balB; [exact: r1|exists y2]. +Qed. + HB.structure Definition NbhsLmodule (K : numDomainType) := {M of Nbhs M & GRing.Lmodule K M}. @@ -83,9 +157,45 @@ HB.structure Definition NbhsLmodule (K : numDomainType) := HB.structure Definition PreTopologicalLmodule (K : numDomainType) := {M of Topological M & GRing.Lmodule K M}. +Section properties_of_preTopologicalLmodule. +Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E). + +Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) (x : E) : + nbhs x U -> nbhs (-x) (-%R @` U). +Proof. +move=> Ux; move: (f (-1, -x) U); rewrite /= scaleN1r opprK => /(_ Ux) [] /=. +move=> [B] B12 [B1 B2] BU; near=> y; exists (- y); 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)) : + nbhs 0 U -> nbhs 0 (-%R @` U). +Proof. by move => Ux; rewrite -oppr0; exact: nbhsN_subproof. Qed. + +Lemma nbhsD_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) : + nbhs 0 U -> nbhs x (+%R x @` U). +Proof. +move => U0; have /= := f (x, -x) U; rewrite subrr => /(_ U0). +move=> [B] [B1 B2] BU; near=> x0. +exists (x0 - x); last by rewrite addrC subrK. +by apply: (BU (x0, -x)); 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 + x.2)) (z x : E) : + nbhs z U -> nbhs (x + z) (+%R x @` U). +Proof. +move=> U0; have /= := f (x + z, -x) U; rewrite [x + z]addrC addrK. +move=> /(_ U0)[B] [B1 B2] BU; near=> x0. +exists (x0 - x); last by rewrite addrC subrK. +by apply: (BU (x0, -x)); split; [near: x0; rewrite nearE|exact: nbhs_singleton]. +Unshelve. all: by end_near. Qed. + +End properties_of_preTopologicalLmodule. + HB.mixin Record TopologicalZmodule_isTopologicalLmodule (R : numDomainType) M & PreTopologicalLmodule R M := { - scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; + scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) }. #[short(type="topologicalLmodType")] @@ -127,10 +237,119 @@ Unshelve. all: by end_near. Qed. End TopologicalLmodule_theory. +Section TopologicalLmodule_numDomain. +Context {R : numDomainType} (E : topologicalLmodType R). + +Lemma nbhs0N (U : set E) : nbhs 0 U -> nbhs 0 (-%R @` U). +Proof. exact/nbhs0N_subproof/scale_continuous. Qed. + +Lemma nbhsD0 (U : set E) (x : E) : nbhs 0 U -> nbhs x (+%R x @` U). +Proof. exact/nbhsD_subproof/add_continuous. Qed. + +Lemma nbhsD (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). +Proof. exact/nbhsB_subproof/add_continuous. Qed. + +Lemma openD (V : set E) (x : E) : open V -> open (+%R x @` V). +Proof. +rewrite openE /= => openV z /= [y uy <-]; rewrite /interior /=. +by apply: nbhsD; rewrite nbhsE /=; exists V => //; split => //; rewrite openE. +Qed. + +Lemma openB (V : set E) (x : E) : open (+%R x @` V) -> open V. +Proof. +suff : V = +%R (- x) @` (+%R x @` V) by move => + H => ->; exact: openD. +apply/seteqP; split => z /=. + move=> Uz; exists (z + x); first by exists z => //; rewrite addrC. + by rewrite addrCA addrA subrK. +by move=> [_ [y' Uy' <-] <-]; rewrite addrCA addrA subrr add0r. +Qed. + +Lemma nbhsE0 (x : E) (b : set E): nbhs x b <-> b x /\ + exists2 a, nbhs 0 a & [set x + x0 | x0 in a] `<=` b. +Proof. +split. + move => /[dup] /(nbhsD (-x)); rewrite addNr => nb0 nb; split. + exact: nbhs_singleton. + exists [set - x + x0 | x0 in b] => // z /=. + by move=> [y /= [y' by']] <- <-; rewrite addrA addrN add0r. +move=> [bx [a n0a xab]]; apply: filterS; first exact: xab. +exact: nbhsD0. +Qed. + +End TopologicalLmodule_numDomain. + +Section TopologicalLmodule_numField. + +Lemma openZ (R : numFieldType) (E : topologicalLmodType R) (U : set E) (r : R) : + r != 0 -> open U -> open ( *:%R r @` U ). +Proof. +move=> r0; rewrite openE /interior /= => openU z /= [x Ux <-]. +apply: nbhsZ => //. +by rewrite nbhsE => /=; exists U => //; split; rewrite // openE. +Qed. + +End TopologicalLmodule_numField. + +Section TopologicalLmodule_theory. +Context {E : Type} {R : numFieldType} {F G : topologicalLmodType R}. + +Lemma continuousfor0_continuous (f : {linear F -> G}) : + {for 0, continuous f} -> continuous f. +Proof. +move=> cont0 x. +suff: (f y - f x)@[y --> x] --> (0 : G). + have -> : (fun y => f y - f x) = (fun y => f (y - x)). + by apply/funext => y; rewrite linearB. + move=> fxfy /= A nA /=. + pose B := [set y - f x | y in A]. + have /fxfy : nbhs 0 B. + have -> : B = (+%R^~ (- (- f x))) @^-1` A. + rewrite opprK; apply/seteqP; split. + by move=> y [/= g Ag <-]; rewrite subrK. + move=> g/= Agfx; eexists; first exact: Agfx. + by rewrite addrK. + have:= @continuous_shift _ (0 : G) (f x) A. + by rewrite opprK add0r => /(_ nA); exact. + rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=. + by move=> [y Ay]; rewrite linearB => /subIr <-. +have -> : (fun y => f y - f x) = (fun y => f (y - x)). + by apply/funext => y; rewrite linearB. +apply: cvg_comp; last by rewrite -(linear0 f); exact: cont0. +by move => A nA /=; apply: continuous_shift; rewrite subrr. +Qed. + +End TopologicalLmodule_theory. + +Section topologicalLmodType_realFieldType. + +(*better naming ?*) +Lemma scalerx_continuous (R : realFieldType) (E : topologicalLmodType R) (x : E) + (s : R) : + {for s, continuous (fun t : R^o => t *: x)}. +Proof. +have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)). + exact: funext. +apply: continuous_comp. +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. +exact: (scale_continuous (s, x)). +Qed. + +Lemma scalexr_continuous (R : realFieldType) (E : topologicalLmodType R) (x : E) + (s : R) : + {for x, continuous (fun y : E => s *: y)}. +Proof. +have -> : (fun y : E => s *: y) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). + exact: funext. +apply: continuous_comp. +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. +exact: (scale_continuous (s, x)). +Qed. + +End topologicalLmodType_realFieldType. + HB.factory Record TopologicalNmodule_isTopologicalLmodule (R : numDomainType) M & PreTopologicalLmodule R M := { - scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) ; -}. + scale_continuous : continuous (fun z : R^o * M => z.1 *: z.2) }. HB.builders Context R M & TopologicalNmodule_isTopologicalLmodule R M. @@ -155,13 +374,24 @@ HB.end. HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E & Uniform E & GRing.Lmodule R E := { locally_convex : exists2 B : set_system E, - (forall b, b \in B -> convex_set b) & basis B + (forall b, b \in B -> absolutely_convex_set b) & (nbhs_basis 0) B }. +(* NB : it is enough to ask for convex_set only and show that +absolutely_convex_set can be derived from it, by taking the absolute_convex closure *) #[short(type="convexTvsType")] HB.structure Definition ConvexTvs (R : numDomainType) := {E of Uniform_isConvexTvs R E & UniformZmodule E & TopologicalLmodule R E}. +HB.mixin Record isSubConvexSpace (R : numDomainType) (V : convType R) + (S : pred V) U & SubChoice V S U & ConvexSpace R U := { + valconv : forall (t : {i01 R}) (a b : U), val (conv t a b) = conv t (val a) (val b) +}. + +#[short(type="subConvType")] +HB.structure Definition SubConvexSpace (R : numDomainType) (V : convType R) S := + { U of SubChoice V S U & ConvexSpace R U & isSubConvexSpace R V S U }. + #[short(type="subConvexTvsType")] HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) (S : pred V) := @@ -170,11 +400,13 @@ HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) Section SubLmodule_isSubConvexTvs. Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). -Local Notation sub_init_topo := (sub_initial_topology U). -HB.instance Definition _ := Uniform.on sub_init_topo. -HB.instance Definition _ := GRing.Lmodule.on sub_init_topo. +Definition init_subconvextvs := sub_initial_topology U. -Let add_sub: continuous (fun x : sub_init_topo * sub_init_topo => x.1 + x.2). +HB.instance Definition _ := Uniform.on init_subconvextvs. +HB.instance Definition _ := GRing.Lmodule.on init_subconvextvs. + +Let add_sub : continuous + (fun x : init_subconvextvs * init_subconvextvs => x.1 + x.2). Proof. apply: continuous_comp_initial => -[/= x y]. pose h := fun xy : U * U => (\val xy.1, \val xy.2). @@ -183,28 +415,25 @@ rewrite (_ : _ \o _ = g \o h). by apply/funext => i /=; rewrite GRing.valD. apply: continuous_comp; last exact: add_continuous. apply: cvg_pair => //=. -- apply: (cvg_comp _ _ cvg_fst). - exact: (continuous_valE (x : sub_init_topo)). -- apply: (cvg_comp _ _ cvg_snd). - exact: (continuous_valE (y : sub_init_topo)). +- exact/(cvg_comp _ _ cvg_fst)/continuous_valE. +- exact/(cvg_comp _ _ cvg_snd)/continuous_valE. Qed. HB.instance Definition _ := - @PreTopologicalNmodule_isTopologicalNmodule.Build sub_init_topo add_sub. + @PreTopologicalNmodule_isTopologicalNmodule.Build init_subconvextvs add_sub. -Let opp_sub : continuous (-%R : sub_init_topo -> sub_init_topo). +Let opp_sub : continuous (-%R : init_subconvextvs -> init_subconvextvs). Proof. apply: continuous_comp_initial => x. rewrite (_ : _ \o _ = -%R \o \val). by apply/funext=> i /=; rewrite GRing.valN. -apply: continuous_comp; first exact: continuous_valE. -exact: opp_continuous. +by apply: continuous_comp; [exact: continuous_valE|exact: opp_continuous]. Qed. HB.instance Definition _ := - TopologicalNmodule_isTopologicalZmodule.Build sub_init_topo opp_sub. + TopologicalNmodule_isTopologicalZmodule.Build init_subconvextvs opp_sub. -Let scale_sub : continuous (fun z : R^o * sub_init_topo => z.1 *: z.2). +Let scale_sub : continuous (fun z : R^o * init_subconvextvs => z.1 *: z.2). Proof. apply: continuous_comp_initial => - [] /= x /= y. pose h := fun xy : R * U => (xy.1, \val xy.2). @@ -212,7 +441,7 @@ pose g := fun xy : R * V => xy.1 *: xy.2. rewrite (_ : _ \o _ = g \o h); first by apply/funext=> i /=; rewrite GRing.valZ. apply: continuous_comp; last exact: scale_continuous. move=> /= A [/= [/= B C]] [[r/= r0 xrB]]. -move/(continuous_valE (y : sub_init_topo)) => [/= C' [woC' C'y C'C] BCA]. +move/(continuous_valE (y : init_subconvextvs)) => [/= C' [woC' C'y C'C] BCA]. apply: filterS; first exact: BCA. exists (ball x r, C') => /=. by split; [exact: nbhsx_ballx|exists C'; split]. @@ -220,10 +449,10 @@ by move=> su/= [xru C'u]; split; [exact: xrB|exact: C'C]. Qed. HB.instance Definition _ := - TopologicalZmodule_isTopologicalLmodule.Build R sub_init_topo scale_sub. + TopologicalZmodule_isTopologicalLmodule.Build R init_subconvextvs scale_sub. Let add_unif_continuous : - unif_continuous (fun x : sub_init_topo * sub_init_topo => x.1 + x.2). + unif_continuous (fun x : init_subconvextvs * init_subconvextvs => x.1 + x.2). Proof. apply/initial_unif_continuous_comp. rewrite (_ : _ \o _ = (fun x => x.1 + x.2) \o (fun x => (val x.1, val x.2)))/=. @@ -235,9 +464,9 @@ by apply: pair_unif_continuous => //=; Qed. HB.instance Definition _ := - PreUniformNmodule_isUniformNmodule.Build sub_init_topo add_unif_continuous. + PreUniformNmodule_isUniformNmodule.Build init_subconvextvs add_unif_continuous. -Let opp_unif_continuous : unif_continuous (-%R : sub_init_topo -> sub_init_topo). +Let opp_unif_continuous : unif_continuous (-%R : init_subconvextvs -> init_subconvextvs). Proof. apply/initial_unif_continuous_comp. rewrite (_ : _ \o _ = (fun x => - x) \o val)/=. @@ -247,65 +476,45 @@ by apply: unif_continuous_comp; Qed. HB.instance Definition _ := - UniformNmodule_isUniformZmodule.Build sub_init_topo opp_unif_continuous. + UniformNmodule_isUniformZmodule.Build init_subconvextvs opp_unif_continuous. Local Open Scope convex_scope. -Let locally_convex_sub : exists2 B : set_system sub_init_topo, - (forall b, b \in B -> convex_set b) & basis B. -Proof. -have [B convexB [openB/= genB]] := @locally_convex R V. -exists [set a | exists2 b, B b & \val @^-1` b = a]. - move=> a /[!inE]/= -[b Bb ba] r s l ra sa. - suff : \val (r <|l|> s) \in b by rewrite !inE /= -ba. - rewrite !GRing.valD !GRing.valZ convexB//; first exact: mem_set. - - by move: ra; rewrite -ba !inE. - - by move: sa; rewrite -ba !inE. -split => /=. - move=> a/= [b Bb <-]; rewrite /open/= /initial_open/=; exists b => //. - exact: openB. -move=> x a [/= b [[/=c openc] cb bx ba]]. -rewrite /nbhs/= /filter_from/=. -have : nbhs (val x) c. - rewrite nbhsE /=; exists c => //; split => //. - by move: bx; rewrite -cb. -move/genB => [d [Bd dx dc]]. -exists (\val @^-1` d); first by split => //; exists d. -by move=> y dy; apply: ba; rewrite -cb; exact: dc. +Let locally_convex_sub : exists2 B : set_system init_subconvextvs, + (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. +Proof. +have [B absconvB [B0 nbhsb]] := @locally_convex R V. +rewrite /filter_from /= in nbhsb. +exists [set \val @^-1` b | b in B]. + move=> a; rewrite inE /= => -[b] /mem_set/absconvB [convb balb] <-; split. + move => r s l ra sa; suff : \val (r <|l|> s) \in b by []. + by rewrite !GRing.valD !GRing.valZ convb. + move=> /= r r1 x /= [rx] ? <-; apply: balb => /=; first exact: r1. + by exists (\val rx); rewrite ?GRing.valZ. +split. + move=> ? /= [b /B0] + <-. + rewrite -[X in nbhs X _ -> _](linear0 (\val : U -> V)). + exact: initial_nbhs_preimage. +move=> /= A [a' [/= [/= b ob <-] /= b0 ba]]. +have /nbhsb [b' Bb bb'] : nbhs 0 b. + by apply: open_nbhs_nbhs; split; rewrite -?(linear0 (\val : U -> V)). +by exists (val @^-1` b') => /=; [exists b'|move => x /= /bb' /ba]. Qed. Local Close Scope convex_scope. HB.instance Definition _ := - @Uniform_isConvexTvs.Build R sub_init_topo locally_convex_sub. -HB.instance Definition _ := GRing.SubLmodule.on sub_init_topo. + @Uniform_isConvexTvs.Build R init_subconvextvs locally_convex_sub. +HB.instance Definition _ := GRing.SubLmodule.on init_subconvextvs. End SubLmodule_isSubConvexTvs. -Section properties_of_topologicalLmodule. -Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E). - -Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) (x : E) : - nbhs x U -> nbhs (-x) (-%R @` U). -Proof. -move=> Ux; move: (f (-1, -x) U); rewrite /= scaleN1r opprK => /(_ Ux) [] /=. -move=> [B] B12 [B1 B2] BU; near=> y; exists (- y); 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)) : - nbhs 0 U -> nbhs 0 (-%R @` U). -Proof. by move => Ux; rewrite -oppr0; exact: nbhsN_subproof. Qed. - -End properties_of_topologicalLmodule. - HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) E & PreTopologicalLmodule 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_system E, - (forall b, b \in B -> convex_set b) & basis B + (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B }. HB.builders Context R E & PreTopologicalLmod_isConvexTvs R E. @@ -317,11 +526,11 @@ Definition entourage : set_system (E * E) := Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U). Proof. exact/nbhs0N_subproof/scale_continuous. Qed. -Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U). +Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (- x) (-%R @` U). Proof. exact/nbhsN_subproof/scale_continuous. Qed. -Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). -Proof. exact/nbhsT_subproof/add_continuous. Qed. +Let nbhsD (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). +Proof. exact/nbhsD_subproof/add_continuous. Qed. Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U). Proof. exact/nbhsB_subproof/add_continuous. Qed. @@ -334,7 +543,7 @@ split; first by exists [set: E]; split; first exact: filter_nbhsT. exists (U `&` V); split => [|xy]. by exists (B `&` C); [exact: open_nbhsI|exact: setISS]. by rewrite !in_setI => /andP[/Bxy-> /Cxy->]. -by move=> P Q PQ [U [HU Hxy]]; exists U; split=> [|xy /Hxy /[!inE] /PQ]. +by move=> P Q PQ [U [HU Hxy]]; exists U; split => [|xy /Hxy /[!inE] /PQ]. Qed. Let entourage_refl (A : set (E * E)) : @@ -383,7 +592,7 @@ apply/funext => U; apply/propext => /=; rewrite /entourage /=; split. move=> Uxy; exists (v - x); last by rewrite addrC subrK. 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). + near: z; rewrite nearE; have := nbhsD x (nbhs0N nU). rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U0])//. apply/funext => /= z /=; apply/propext; split. by move=> [x0] [x1 Ux1 <-] <-; rewrite opprB addrC subrK inE. @@ -396,9 +605,11 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_inv entourage_split_ex nbhsE. -HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. +HB.instance Definition _ := + PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. -HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. +HB.instance Definition _ := + TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. Let nbhs0_split (U : set E) : nbhs 0 U -> exists2 V : set E, nbhs 0 V & forall u v, V u -> V v -> U (u + v). @@ -447,16 +658,288 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. -Section ConvexTvs_numDomain. -Context {R : numDomainType} (E : convexTvsType R) (U : set E). +HB.factory Record NbhsBasisAt0_isConvexTvs (R : numFieldType) E + & GRing.Lmodule R E := { + nbhsbasis_at0 : set_system E ; + nonempty_nbhsbasis_at0 : nbhsbasis_at0 !=set0 ; + mem0_nbhsbasis_at0 : forall B, nbhsbasis_at0 B -> B 0 ; + absorbing_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absorbing_set _ E ; + absconvex_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absolutely_convex_set _ E ; + expand_nbhsbasis_at0 : forall B r, nbhsbasis_at0 B -> + exists2 U, nbhsbasis_at0 U & ( *:%R r) @` U `<=` B ; + nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> + exists2 W, nbhsbasis_at0 W & W `<=` U `&` V }. -Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). -Proof. exact/nbhs0N_subproof/scale_continuous. Qed. +Definition filter_from_basis0 (R : numFieldType) (E : zmodType) + (nbhsbasis_at0 : set_system E) (x : E) := + filter_from [set U | exists2 V, nbhsbasis_at0 V & [set x] `+ V = U] id. + +HB.builders Context R E & NbhsBasisAt0_isConvexTvs R E. + +Let nbhs_fromfilter0 := @filter_from_basis0 R E (nbhsbasis_at0). + +#[local] Lemma split_nbhsbasis_at0 B : nbhsbasis_at0 B -> + exists2 C, nbhsbasis_at0 C & C `+ C `<=` B. +Proof. +move=> /(@expand_nbhsbasis_at0 _ 2)[U fU UB]. +exists U => //= x [u Uu] [v Uv] <-. +apply: UB. +exists (2^-1 *: (u + v)); last by rewrite scalerA mulfV// scale1r. +rewrite scalerDr. +have [convU _] := absconvex_nbhsbasis_at0 fU. +have H : 0 <= 2^-1 :> R by []. +have G : 2^-1 <= 1 :> R by rewrite invf_le1 ?lerDl. +pose r := Itv01 H G. +have := convU u v r. +rewrite !inE => /(_ Uu Uv); rewrite /conv/=. +suff -> : (2^-1).~ = 2^-1 :> R by []. +by rewrite /onem [X in X - _](splitr 1) div1r addrK. +Qed. + +Let nbhs_filter (p : E) : ProperFilter (nbhs_fromfilter0 p). +Proof. +apply: filter_from_proper. + apply: filter_from_filter => /=. + have [U fU] := nonempty_nbhsbasis_at0. + by exists ([set p] `+ U) => //=; exists U. + move=> _ _ /= [U0 FU <-] [V0 FV <-]. + have [W FW WUV] := nbhsbasis_at0I FU FV. + exists ([set p] `+ W); first by exists W. + by rewrite -addsetI; exact: addsetS. +move=> _ /= [V FV] <-. +by exists p, p => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasis_at0. +Qed. + +Let nbhs_singleton (p : E) (A : set E) : nbhs_fromfilter0 p A -> A p. +Proof. +move=> [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. +exact: mem0_nbhsbasis_at0. +Qed. + +Let nbhs_nbhs (p : E) (A : set E) : nbhs_fromfilter0 p A -> + nbhs_fromfilter0 p (nbhs_fromfilter0^~ A). +Proof. +rewrite /nbhs_fromfilter0/=. +move=> [B/= [C f0C <- pCA]] //=. +have [D f0D DDC] := split_nbhsbasis_at0 f0C. +exists ([set p] `+ D); first by exists D. +move=> _ [/= _] -> [c Cc <-] /=. +exists ([set p + c] `+ D) => //; first by exists D. +apply: (subset_trans _ pCA). +apply: (@subset_trans _ ([set p] `+ ([set c] `+ D))); first by exact: addsetA. +apply: addsetS => //; apply: subset_trans DDC; apply: addsetS => //. +by move=> x ->. +Qed. + +HB.instance Definition _ := @hasNbhs.Build E nbhs_fromfilter0. + +HB.instance Definition _ := + @Nbhs_isNbhsTopological.Build E nbhs_filter nbhs_singleton nbhs_nbhs. + +Let add_continuous : continuous (fun x : E * E => x.1 + x.2). +Proof. +move=> /= [x1 x2] /= A /= [V] /= [V0 filterV0 <-{V}] VA. +have [W filter0W WV] := split_nbhsbasis_at0 filterV0. +exists ([set x1] `+ W, [set x2] `+ W) => /=. +split => //=; first by exists ([set x1] `+ W) => //; exists W. +exists ([set x2] `+ W) => //; exists W => //. +move => [z1 z2] /= [[x ->]] => [[y1] Vy <-{z1}]. +move => [t ->{t}] [y2 Wy2 <-]. +apply: VA => //=. +exists (x1 + x2) => //; exists (y1 + y2). +apply: WV =>/=; exists y1 => //; exists y2 => //. +by rewrite addrACA. +Qed. + +Let scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2). +Proof. +move => /= [r x] /= A /= [_] /= [V fV <-] VA. +have [r0|] := eqVneq r 0. + have [V0 fV0 rV0] := split_nbhsbasis_at0 fV. + have [/= s s0] := absorbing_nbhsbasis_at0 fV0 x. + rewrite inE => xV''. + have [convV'' balV''] := absconvex_nbhsbasis_at0 fV0. + exists ((ball_ normr 0 (minr 1 s)), [set x] `+ V0) => //=. + split. + exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //. + by rewrite r0. + by exists ([set x] `+ V0) => //; exists V0. + move => [z1 z2] /=; rewrite sub0r normrN => -[z1s]. + move=> [_ ->] [y] Vy <- {z2}; apply: VA => /=. + rewrite r0; exists 0; rewrite ?scale0r//. + exists (z1 *: (x + y)); rewrite ?add0r//. + apply: rV0 => /=; exists (z1 *: x). + apply: (balV'' (z1 * s^-1)). + rewrite normrM normfV ltW// ltr_pdivrMr ?normr_gt0 ?gt_eqF//. + rewrite mul1r [ltRHS]gtr0_norm // (lt_le_trans z1s) //. + by rewrite /minr; case: ifPn => // /ltW. + by exists (s *: x) => //; rewrite !scalerA divfK// gt_eqF //. + exists (z1 *: y) => //; last by rewrite -scalerDr. + apply: (balV'' z1); last by exists y. + by rewrite (le_trans (ltW z1s)) // /minr; case: real_ltP => //; + rewrite gtr0_real. +have [V0 fV0 rV0] := split_nbhsbasis_at0 fV. +have [V' fV' rV'] := split_nbhsbasis_at0 fV0. +have [V'' fV'' rV''] := expand_nbhsbasis_at0 r fV'. +have [/= s s0] := absorbing_nbhsbasis_at0 fV'' x. +rewrite inE => xV''. +have [convV'' balV''] := absconvex_nbhsbasis_at0 fV''. +exists ([set r] `+ (ball_ normr 0 (Num.min `|r| `|r * s|)), [set x] `+ V'') => //=. + split; last by exists ([set x] `+ V'') => //; exists V''. + exists (Num.min `|r| `|r * s|) => //=. + rewrite /minr; case: ifPn; first by rewrite normr_gt0. + by rewrite normr_gt0 => _ ; rewrite mulf_neq0 // gt_eqF. + move=> u/= rur; exists r => //; exists (u - r); last by rewrite subrKC. + by rewrite sub0r normrN distrC (lt_le_trans rur). +move => [z1 z2] /= => [] [[x0] -> {x0}] [y]; rewrite add0r normrN => yr. +move => <- [H ->] [t] Vt <-; apply: VA => /=. +exists (r *: x) => //; exists (r *: t + y *: x + y *: t); last first. + by rewrite !addrA -scalerDr -addrA -scalerDr scalerDl. +apply: rV0; exists (r *: t) => //. + apply: rV'; exists 0; first by apply: mem0_nbhsbasis_at0. + exists (r *: t); first by apply: rV''; exists t. + by rewrite add0r. +exists (y *: x + y *: t); last by rewrite addrA. +apply: rV'; exists (y *: x). +apply: rV''. + exists ((r^-1 * y) *: x). + apply: (balV'' (r^-1 * y * s^-1)). + rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1. + rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0//. + rewrite (le_trans (ltW yr))//. + rewrite /minr; case: ifPn; last by move=> _; rewrite normfV normrM invrK. + by move/ltW; rewrite normrM normfV invrK. + exists (s *: x); rewrite // !scalerA divfK// gt_eqF//. + by rewrite scalerA mulrA divff// mul1r. +exists (y *: t) => //; apply: rV''; exists ((r^-1 * y) *: t); last first. + by rewrite scalerA mulrA divff// mul1r. +apply: (balV'' (r^-1 * y)); last by exists t. +rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1. +by apply: (le_trans (ltW yr)); rewrite /minr; case: real_ltP. +Qed. + +Let locally_convex : exists2 B : set_system E, + (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B. +Proof. +exists nbhsbasis_at0. + by move=> b; rewrite inE; apply: absconvex_nbhsbasis_at0. +split; first by move=> /= A nA; exists A => //; exists A => //; rewrite add0set. +move => b [a] /= [a'] fa; rewrite add0set => <- ab /=. +by exists a' => //=; split => //; exact: mem0_nbhsbasisat0. +Qed. + +HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E + add_continuous scale_continuous locally_convex. + +HB.end. + +HB.factory Record NbhsSubbasisAt0_isConvexTvs (R : numFieldType) E + & GRing.Lmodule R E := { + nbhssubbasis_at0 : set_system E ; + nonempty_nbhssubbasis_at0 : nbhssubbasis_at0 !=set0 ; + mem0_nbhssubbasis_at0 : forall B, nbhssubbasis_at0 B -> B 0 ; + absorbing_nbhssubbasis_at0 : nbhssubbasis_at0 `<=` @absorbing_set _ E ; + absconvex_nbhssubbasis_at0 : nbhssubbasis_at0 `<=` @absolutely_convex_set _ E ; + expand_nbhssubbasis_at0 : forall B r, nbhssubbasis_at0 B -> + exists2 U, nbhssubbasis_at0 U & ( *:%R r) @` U `<=` B }. + +Definition finI_fromsubbasis0 (R : numFieldType) (E : zmodType) + (nbhssubbasis0 : set_system E) := + finI_from nbhssubbasis0 id. -Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). -Proof. exact/nbhsT_subproof/add_continuous. Qed. +HB.builders Context R E & NbhsSubbasisAt0_isConvexTvs R E. -End ConvexTvs_numDomain. +Let nbhsbasis_at0 := @finI_fromsubbasis0 R E nbhssubbasis_at0. + +Let nonempty_nbhsbasisat0 : nbhsbasis_at0 !=set0. +Proof. +have [U fU] := nonempty_nbhssubbasis_at0; exists U. +rewrite /nbhsbasis_at0 /finI_fromsubbasis0 /finI_from /=. +exists [fset U]%fset => /=. + by move=> _ /fset1P ->; rewrite mem_set //=; exists U; rewrite ?addset0. +by rewrite bigcap_fset big_seq_fset1. +Qed. + +Let nbhsbasis_at0I U V : nbhsbasis_at0 U -> nbhsbasis_at0 V -> + exists2 W, nbhsbasis_at0 W & W `<=` U `&` V. +Proof. +move=> [/= I fI IV] [/= J fJ JU]. +exists (U `&` V) => //; exists (I `|` J)%fset. + move => /= W; rewrite !inE => /orP [WI|WJ]. + by have := fI _ WI; rewrite asboolE. + by have := fJ _ WJ; rewrite asboolE. +by rewrite -IV -JU -bigcap_setU set_fsetU. +Qed. + +Let mem0_nbhsbasis_at0 B : nbhsbasis_at0 B -> B 0. +Proof. by move=> [/= I fI <-] U /= /fI /= /set_mem /mem0_nbhssubbasis_at0. Qed. + +Let expand_nbhsbasis_at0 B r : nbhsbasis_at0 B -> + exists2 U, nbhsbasis_at0 U & ( *:%R r) @` U `<=` B. +Proof. +move=> [/= I fI BI]. +have H i : (i \in I) -> exists2 V, nbhssubbasis_at0 V & ( *:%R r) @` V `<=` i. + move=> /(fI i); rewrite asboolE => /(expand_nbhssubbasis_at0 r) /= [V nV rVi]. + by exists V. +pose f i := if (i \in I) =P true is ReflectT h then sval (cid2 (H _ h)) else setT. +have Hn i : i \in I -> nbhssubbasis_at0 (f i). + by rewrite /f; case: eqP => // h _; case: cid2. +have Hr i : i \in I -> ( *:%R r) @` f i `<=` i. + by rewrite /f; case: eqP => // h _; case: cid2. +pose U := \bigcap_(i in [set` I])(f i). +exists U. exists (f @` I)%fset => /=. + - by move => _ /imfsetP[/= b bi ->]; exact/mem_set/Hn. + - by rewrite set_imfset bigcap_image. +rewrite -BI => x /= [y]; rewrite /U /= => Uy rx i /= j. +apply: Hr => //=. +by exists y => //; exact: Uy. +Qed. + +Let absorbing_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absorbing_set _ E. +Proof. +move=> B [/= I fI BI] /= x. +have /= H : forall i, i \in I -> exists r : {posnum R}, r%:num *: x \in i. + move => i /(fI i); rewrite asboolE => /absorbing_nbhssubbasis_at0/(_ x)[r r0 rx]. + by exists (PosNum r0). +pose f (i : set E) : {posnum R} := + [elaborate if (i \in I) =P true is ReflectT h then sval (cid (H i h)) else 1%:pos]. + (*why is elaborate necessary here ???*) +have /= Hr i : i \in I -> (f i)%:num *: x \in i. + by rewrite /f; case: eqP => // h _; case: cid. +pose r0 : {posnum R} := [elaborate \big[Order.min/1%:pos]_(i <- I) f i]. +exists r0%:num => //. +rewrite -BI asboolE /= => i /= iI. +have ni : nbhssubbasis_at0 i by apply/set_mem/fI. +have [_ bali] := absconvex_nbhssubbasis_at0 ni. +apply: (bali (r0%:num / (f i)%:num)). + rewrite ger0_norm // ler_pdivrMr // mul1r /r0 num_le //. + exact: ge_bigmin_seq. +exists ((f i)%:num *: x); first exact/set_mem/Hr. +by rewrite scalerA mulfVK. +Qed. + +Let absconvex_nbhsbasis_at0 : nbhsbasis_at0 `<=` @absolutely_convex_set _ E. +Proof. +move=> B [/= I fI <-]; split. + move=> x y r; rewrite !asboolE /= => xb yb => // i /= iI. + have /fI := iI; rewrite asboolE; move=> /absconvex_nbhssubbasis_at0[+ _]. + move=> /(_ x y r); rewrite !asboolE; apply; first exact: xb. + exact: yb. +move=> r r1 x /= [y] capy <- i /= iI. +have /fI := iI; rewrite asboolE => /absconvex_nbhssubbasis_at0[_ +]. +by move=> /(_ r r1 (r *: y)); apply => /=; exists y => //; exact: capy. +Qed. + +HB.instance Definition _ := @NbhsBasisAt0_isConvexTvs.Build R E + nbhsbasis_at0 nonempty_nbhsbasisat0 mem0_nbhsbasis_at0 absorbing_nbhsbasis_at0 + absconvex_nbhsbasis_at0 expand_nbhsbasis_at0 nbhsbasis_at0I. + +HB.end. + +Section ConvexTvs_realType. + + +End ConvexTvs_realType. Section standard_topology. Context {R : numFieldType}. @@ -467,8 +950,7 @@ Let standard_ball_convex_set (x : R^o) (r : R) : convex_set (ball x r). Proof. apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1. rewrite inE/=. -rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |> - (x - y : convex_lmodType _)). +rewrite [X in `|X|](_ : _ = (x - z) <| l |> (x - y)). by rewrite opprD -[in LHS](convmm l x) addrACA -scalerBr -scalerBr. rewrite (le_lt_trans (ler_normD _ _))// !normrM. rewrite (@ger0_norm _ l%:num)// (@ger0_norm _ l%:num.~) ?onem_ge0//. @@ -476,14 +958,23 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl. by rewrite ltrD// ltr_pM2l// onem_gt0. Qed. +Let standard_ball_balanced_set (r : R) : balanced_set (ball (0 : R^o) r). +Proof. +move=> t /= t1 z /= [y]. +rewrite -ball_normE /= !sub0r !normrN => + <-. +by rewrite normrM; apply: le_lt_trans; rewrite ler_piMl. +Qed. + Let standard_locally_convex_set : - exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B. + exists2 B : set_system R^o, (forall b, b \in B -> absolutely_convex_set b) & + nbhs_basis 0 B. Proof. -exists [set B | exists x r, B = ball x r]. - by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set. -split; first by move=> B [x] [r] ->; exact: ball_open. -move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. -by exists (ball x r) => //=; split; [exists x, r|exact: ballxx]. +exists [set B | exists2 r, 0 < r & B = ball 0 r]. + move=> B /[!inE]/= -[r _ ->]; split. + - exact: standard_ball_convex_set. + - exact: standard_ball_balanced_set. +split; first by move=> /= ? [r r0 ->]; exact: nbhsx_ballx. +by move=> /= B [r r0 Br]; exists (ball 0 r); [exists r|exact: Br]. Qed. HB.instance Definition _ := @@ -510,28 +1001,23 @@ by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split; Qed. Local Lemma prod_locally_convex : - exists2 B : set_system (E * F), (forall b, b \in B -> convex_set 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]. -split. - by apply/set_mem/Bcb; [exact/mem_set|exact/mem_set|exact/mem_set]. -by apply/set_mem/Bcf; [exact/mem_set|exact/mem_set|exact/mem_set]. + exists2 B : set_system (E * F), (forall b, b \in B -> absolutely_convex_set b) + & nbhs_basis (0, 0) B. +Proof. +have [Be Bce [Be0 Beb]] := @locally_convex K E. +have [Bf Bcf [Bf0 Bfb]] := @locally_convex K F. +pose B := [set be `*` bf | be in Be & bf in Bf]. +have B00 : nbhs_basis (0, 0) B. + split. + by move=> /= b [be ?] [bf ?] <-; exists (be, bf) => //=; split => //; + [exact/Be0|exact/Bf0]. + move=> /= b [[/= be bf] [/= nbe nbf]] befb /=. + have [/= be' Beb' bbe] := Beb be nbe. + have [/= bf' Bfb' bbf] := Bfb bf nbf. + exists (be' `*` bf') => /=; first by exists be' => //; exists bf'. + by apply: subset_trans befb; exact: setSX. +exists B => // b; rewrite inE /= => -[be Bbe] [bf Bbf] <-. +by apply: absolutely_convex_setX; [exact/Bce/mem_set|exact/Bcf/mem_set]. Qed. HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build @@ -546,7 +1032,7 @@ HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.ty (F : NbhsZmodule.type) (s : K -> F -> F) := {f of @GRing.Linear K E F s f & @Continuous E F f }. -(* https://github.com/math-comp/math-comp/issues/1536 +(* see https://github.com/math-comp/math-comp/issues/1536 we use GRing.Scale.law even though it is claimed to be internal *) HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K) (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := { @@ -708,3 +1194,563 @@ Lemma lcfun_linear : linear f. Proof. move => *; exact: linearP. Qed. End lcfunproperties. + +Local Open Scope convex_scope. + +Section openbasis. +Context (R : realType) (E : convexTvsType R). + +Definition nbhsbasis_convextvs := sval (cid2 (@locally_convex _ E)). + +Definition open_nbhsbasis_convextvs := + [set interior b | b in nbhsbasis_convextvs]. + +Local Open Scope convex_scope. + +Lemma has_open_nbhs_basis : + nbhs_basis 0 open_nbhsbasis_convextvs /\ + (forall b, open_nbhsbasis_convextvs b -> open b /\ absolutely_convex_set b). +Proof. +have [absconv [] nbhs0 basis] := svalP (cid2 (@locally_convex _ E)). +split. + split; move=> a /=; first by move=> [b /nbhs0] nbhsb <-; exact: nbhs_interior. + move=> /basis /= [b /= nbhsb ba]; exists (interior b); first by exists b. + by apply: subset_trans ba; exact: interior_subset. +move=> ? /= [b nb <-]; split; first exact: open_interior. +have [convb balb] := absconv b (mem_set nb). +split. + move => x y t; rewrite !inE. + move => /nbhsE0 [bx [ax nax axb]] /nbhsE0 [by' [ay nay ayb]]; apply/nbhsE0. + split. + by apply/set_mem/convb; rewrite !inE. + exists (ax `&` ay); first exact: filterI. + move=> z /= [z' [xz xz'] <-]. + rewrite convD. + apply/set_mem/convb; rewrite inE; first by apply: axb; exists z'. + by apply: ayb; exists z'. +move=> /= t. +have [->|t0] := eqVneq t 0. (*disctinction overlooked in the literature*) + by move=> _ ? /= [?] _; rewrite scale0r => <-; apply: nbhs0 => /=; exact: nb. +move=> t1 ? /= [x] /= + <- => /nbhsE0[bx [a na0 ab]]. +apply/nbhsE0; split. + apply: balb; first exact: t1. + by exists x. +exists (( *:%R t ) @` a). + by rewrite -(@scaler0 _ _ t); apply: nbhsZ => // ? /= [y ay] <-. +move => z /= [?] [y] ax <- <-; rewrite -scalerDr; apply: balb; first exact: t1. +by exists (x + y)=> //; apply: ab; exists y. +Qed. + +Definition open_absconvex_opennbhsbasis := has_open_nbhs_basis.2. + +Definition basis_opennbhsbasis := has_open_nbhs_basis.1. + +Lemma basis_neqset0 (B : set_system E) (x : E) : + filter_from [set U | B U] id --> x -> B !=set0. +Proof. +by move=> /(_ [set: E]) /(_ filterT) [b ? _]; exists b. +Qed. + +Lemma absorbing_opennbhsbasis : open_nbhsbasis_convextvs `<=` @absorbing_set _ E. +Proof. +move=> b Bb x. +have [/(_ b Bb) n0b _] := basis_opennbhsbasis. +move: n0b; rewrite -(scale0r x) => n0b. +have := scalerx_continuous => /(_ _ _ x 0 b n0b) [r] /= r0 b0rb. +exists (r / 2); first exact: divr_gt0. +rewrite inE. +apply: b0rb; rewrite /ball_ /= sub0r normrN normrM !gtr0_norm//. +by rewrite gtr_pMr // invf_lt1 // ltrDl. +Qed. + +End openbasis. + +Import Norm. + +Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) + (absA : absolutely_convex_set A) (absorbA : absorbing_set A) : V -> K := + fun v => inf [set r | (0 < r) /\ v \in (fun x => r *: x) @` A]. + +(* K can be a numDomainType once #1959 is solved *) + +Section gauge. +Context (K : realType) (V : lmodType K) (A : set V) + (absA : absolutely_convex_set A) (absorbA : absorbing_set A). + +Notation gauge_fun := (gauge_fun absA absorbA). + +#[local] Lemma gauge0 : gauge_fun 0 = 0. +Proof. +have /absolutely_convex0 := absA => A0; rewrite /gauge_fun. +have [->|]:= eqVneq A set0. + rewrite [X in inf X]( _ : _ = set0). + by rewrite -subset0 => /= x /=; rewrite image_set0 inE => -[] //. + by rewrite inf0. +set P := (X in inf X). +move/set0P/A0 => {}A0. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + apply: lb_le_inf. + exists 1; rewrite /P/= ltr01 inE/=; split => //. + by exists 0 => //; rewrite scale1r. + by move=> z; rewrite /P /= => -[z0] _; rewrite ltW. +have infle (r : K) : 0 < r -> inf P <= r. + move=> r0. + have Pr : P r by split => //; rewrite inE; exists 0 => //; rewrite scaler0. + by apply: ge_inf => //; exists 0 => z /= [] z0 _; rewrite ltW. +by apply/ler_addgt0Pl => /= r r0; rewrite addr0; exact: infle. +Qed. + +#[local] Lemma gauge_ge0 x : 0 <= gauge_fun x. +Proof. +rewrite /gauge_fun; set P := (X in inf X). +have [->|/set0P P0] := eqVneq P set0; first by rewrite inf0. +by apply: lb_le_inf => // z; rewrite /P /= => -[] z0 _; rewrite ltW. +Qed. + +#[local] Lemma ler_gaugeD x y : gauge_fun (x + y) <= gauge_fun x + gauge_fun y. +Proof. +have A0 : A 0 by move: (absorbA 0) => [? ?]; rewrite scaler0 inE. +have := absA; rewrite /absolutely_convex_set => -[] convA /= balA. +have lem1 r w : 0 < r -> A (r *: w) -> w \in [set r^-1 *: x | x in A]. + rewrite inE /=; exists (r *: w) => //. + by rewrite scalerA mulVf ?scale1r ?gt_eqF. +have lem (w : V) : (exists2 r, 0 < r & A (r *: w)) -> + has_inf [set t | 0 < t /\ w \in ( *:%R t) @` A]. + move => [r r0 Aw]; split => /=; rewrite /set0P; last first. + by exists 0 => z [z0 _]; rewrite ltW. + exists r^-1 => //=; split=> //; first by rewrite invr_gt0. + exact: lem1. +rewrite /gauge_fun. +have [/= r r0] := absorbA x; rewrite inE /= => Arx. +have [/= r' r0'] := absorbA y; rewrite inE /= => Ary. +have [/= r2 r20'] := absorbA (x + y); rewrite inE /= => Arxy. +rewrite -inf_sumE; first by apply: lem; exists r. + by apply: lem; exists r'. +apply: infS; first by apply: lem; exists r2. + exists (r^-1 + r'^-1) => /=. + exists r^-1 => //=. + by rewrite invr_gt0 lem1. + exists r'^-1 => //=. + by rewrite invr_gt0 lem1. +move => z /= [t [t0]]; rewrite inE /= => [[v] Av rvx] [s] [s0]; rewrite inE /=. +move => [w Aw twy] <-. +rewrite addr_gt0 => //; split => //; rewrite inE /=. +rewrite -twy -rvx. +exists ((t + s)^-1 *: (t *: v + s *: w)). +rewrite scalerDr !scalerA mulrC (mulrC _ s) -divD_onem => //. +pose st := Itv01 (divDl_ge0 (ltW t0) (ltW s0)) (divDl_le1 (ltW t0) (ltW s0)). +have := convA v w st. +rewrite !inE => /(_ Av Aw); rewrite /conv /=; apply. +by rewrite !scalerA divff ?scale1r //; rewrite gt_eqF // addr_gt0. +Qed. + + +#[local] Lemma gaugeZ r v : gauge_fun (r *: v) = `|r| * gauge_fun v. +Proof. +rewrite /gauge_fun; have [->|] := eqVneq r 0. + rewrite normr0 mul0r. + have A0 : A 0 by move: (absorbA 0)=> [??]; rewrite scaler0 inE. + rewrite [X in inf X](_ : _ = [set r0 | 0 < r0]). + apply/seteqP; split=> [s []//|s /= s0]/=; split => //. + by rewrite inE/=; exists 0 => //; rewrite scale0r scaler0. + exact: inf_pos. +rewrite neq_lt -ge0_infZl// => /orP[r0|r0]; congr inf. +- rewrite ltr0_norm//. + have balA w : A w -> A (- w). + move=> Aw; case: absA => _ /(_ (-1)); apply => /=; first by rewrite normrN1. + by exists w => //; rewrite scaleN1r. + apply/seteqP; split => [x [x0 /[!inE]-[w Aw xwry]]|_ [y [y0 /[!inE]-[w Aw <-{v} <-]]]]/=. + exists ((- r)^-1 * x); last by rewrite invrN mulrA mulrNN divff ?mul1r// lt_eqF. + rewrite mulr_gt0// ?invr_gt0 ?oppr_gt0//; split => //. + rewrite inE/=; exists (- w); first exact: balA. + rewrite scalerN invrN mulNr scaleNr opprK -scalerA xwry scalerA. + by rewrite mulVf ?scale1r ?lt_eqF. + rewrite inE/= mulr_gt0 ?oppr_gt0//; split => //. + exists (- w); first exact: balA. + by rewrite scalerN mulNr scaleNr opprK scalerA. +- rewrite gtr0_norm//. + apply/seteqP; split => [x [x0 /[!inE]-[w Aw xwry]]|_ [y [y0 /[!inE]-[w Aw <-{v} <-]]]]/=. + exists (r^-1 * x); last by rewrite mulrA divff ?mul1r// gt_eqF. + rewrite mulr_gt0 ?invr_gt0 ?gt_eqF//; split => //. + rewrite inE/=; exists w => //. + by rewrite -[LHS]scalerA xwry scalerA mulVf ?scale1r// gt_eqF. + rewrite inE/= mulr_gt0//; split => //. + by exists w => //; rewrite scalerA. +Qed. + +HB.instance Definition _ := @isSemiNorm.Build K V gauge_fun gauge0 + gauge_ge0 ler_gaugeD gaugeZ. + +End gauge. + +Definition seminorm_on {R : realFieldType} {E : lmodType R} + (P : set (SemiNorm.type E)) (Hp : P !=set0) : Type := E. + +Section convex_topology_seminorm. +Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) + (H : P !=set0). + +HB.instance Definition _ := GRing.Lmodule.on (@seminorm_on R E P H). + +Definition seminorm_subbasis : set_system E := + [set A | exists2 p, P p & exists2 e, 0 < e & + A = p @^-1` ball (0 : R) e]. + +Lemma nonempty_subbasis : exists B, seminorm_subbasis B. +Proof. +move : H => [p] Pp. +exists (p @^-1` ball (0 : R) 1). +by exists p => //; exists 1. +Qed. + +Lemma mem0_seminorm_subbasis B : seminorm_subbasis B -> B 0. +Proof. +rewrite /seminorm_subbasis /= => -[p Pp [e]] e0 -> /=; rewrite norm0. +exact: ballxx. +Qed. + +Lemma split_seminorm_subbasis B : seminorm_subbasis B -> + exists2 C, seminorm_subbasis C & C `+ C `<=` B. +Proof. +rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] /=. +exists (p @^-1` ball (0 : R) (e / 2)). + by exists p => //; exists (e / 2); rewrite ?divr_gt0. +rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]. +rewrite sub0r normrN => ballx [y]. +rewrite sub0r normrE => bally <-; rewrite (splitr e). +apply: le_lt_trans; last by apply: ltrD; [exact: ballx|exact: bally]. +(* Beware that now that we opened the Norm module ler_normD refers to semiNorm +and not to norm *) +apply: le_trans; last exact: Num.Theory.ler_normD. +rewrite ger0_le_norm ?nnegrE ?addr_ge0 ?norm_ge0//. +exact: ler_normD. +Qed. + +Lemma expand_seminorm_subbasis B r : seminorm_subbasis B -> + exists2 U, seminorm_subbasis U & ( *:%R r ) @` U `<=` B. +Proof. +rewrite /seminorm_subbasis/= => -[p Pp [e e0 ->]] /=. +have [->|rneq0] := eqVneq r (0 : R). + exists (p @^-1` ball (0 : R) e); first by exists p => //; exists e. + by move => z /= [x] _; rewrite scale0r => <-; rewrite norm0; exact: ballxx. +exists (p @^-1` ball (0 : R) (e / `|r|)). + by exists p => //; exists (e / `|r|); rewrite ?divr_gt0// normr_gt0. +rewrite /ball /= => z /=; rewrite sub0r normrN => -[x]. +rewrite sub0r normrN => ballx <-. +by rewrite normZ normrM normr_id mulrC -ltr_pdivlMr ?normr_gt0. +Qed. + +Lemma convex_seminorm_subbasis : seminorm_subbasis `<=` @convex_set _ E. +Proof. +move=> B ; rewrite /seminorm_subbasis /= => -[p Pp [e e0 ->]] x y r. +rewrite !inE /ball /= !sub0r !normrN => px py. +rewrite /conv /=. +have : `|p (r%:num *: x + r%:num.~ *: y)| <= + `|p (r%:num *: x) + p (r%:num.~ *: y)|. + by rewrite ger0_le_norm ?nnegrE ?addr_ge0 ?norm_ge0 ?ler_normD. +move/le_lt_trans; apply. +rewrite (le_lt_trans (Num.Theory.ler_normD _ _))//. +rewrite !normZ !normrM !normr_id [X in X * _]ger0_norm//. +by rewrite [X in _ + X * _]ger0_norm ?onem_ge0// lt_conv. +Qed. + +Lemma balanced_seminorm_subbasis : seminorm_subbasis `<=` @balanced_set _ E. +Proof. +move => _ [p Pp [r r0] ->] /= s s1 z /= [x]. +rewrite /ball /ball_ /= !sub0r !normrN => pixr <-. +by rewrite normZ normrM normr_id (le_lt_trans _ pixr)// ler_piMl ?normr_ge0. +Qed. + +Lemma absolutely_convex_seminorm_subbasis : + seminorm_subbasis `<=` @absolutely_convex_set _ E. +Proof. +move => b Bb; split; first exact: convex_seminorm_subbasis. +exact: balanced_seminorm_subbasis. +Qed. + +Lemma absorbing_seminorm : seminorm_subbasis `<=` @absorbing_set _ E. +Proof. +move=> B [p Pp [r r0] ->] /= y. +have [y0|y0] := eqVneq (p y) 0. + by exists 1 => //; rewrite scale1r inE /ball/ball_ /= sub0r normrN y0 normr0. +exists (r / 2 * (p y)^-1). + by rewrite !divr_gt0 // lt_neqAle eq_sym norm_ge0; apply/andP. +(*normr_gt0 not available for seminorms *) +rewrite inE /ball /ball_ /= sub0r normrN !normZ !normrM !normr_id !normfV. +by rewrite -mulrA mulVf ?normr_eq0// mulr1 !gtr0_norm ?gtr_pMr ?invf_lt1 ?ltr1n. +Qed. + +HB.instance Definition _ := @NbhsSubbasisAt0_isConvexTvs.Build R (seminorm_on H) + seminorm_subbasis nonempty_subbasis mem0_seminorm_subbasis absorbing_seminorm + absolutely_convex_seminorm_subbasis expand_seminorm_subbasis. + +(**md Using init-fam (see `initial_topology.v`) does not work as we strongly +need a 0 basis. With init-fam we are considering +``` +nbhs a = [A : set E | exists e , A = [set x | |p(x) - p(a)| < e]], +``` +while working from a 0 basis gives us +``` +nbhs a = [A : set E | exists e , A = [set x | p (x - a) < e]]. +``` +In particular, the continuity of the addition can't be proved in the first case. *) + +Import Norm. + +Lemma continuous_at0_seminorm p : P p -> + continuous_at 0 (p : seminorm_on H -> R). +Proof. +move=> Pp /= /= A [r /= r0] pxrA. +exists (p @^-1` (ball (p 0 : R) r)) => /=; last by move=> z /=; exact: pxrA. +exists (p @^-1` ball (0 : R) r) => /=. + exists [fset (p @^-1` ball (0 : R) r)]%fset => /=. + by move=> t; rewrite 2!inE => /eqP ->; exists p => //; exists r. + apply/seteqP; rewrite /bigcap; split => y //=. + by move => /(_ (p @^-1` ball (0 : R) r)); rewrite inE; apply. + by move => bxr i; rewrite inE => /eqP ->. +apply/seteqP; split => z /=. + move => [? ->] [y]; rewrite /ball /= => bry <- /=; rewrite /ball /=. + by rewrite norm0 (add0r y). +by rewrite norm0 => b0rp; exists 0 => //; exists z => //; rewrite add0r. +Qed. + +Lemma continuous_seminorm x p : P p -> continuous_at x (p : seminorm_on H -> R). +Proof. +move=> Pp. +suff: (p y - p x)@[y --> x] --> (0 : R). + move=> pypx A [r r0] /= pxrA. + have npA := pypx (ball (0 : R^o) r) (nbhsx_ballx (0 : R) r r0) => /=. + exists ([set x] `+ (p @^-1` (ball (0: R) r))) => /=. + exists (p @^-1` (ball (0 : R) r)) => //. + exists [fset p @^-1` (ball (0 : R) r)]%fset. + by move => y; rewrite 2!inE => /eqP ->; exists p => //; exists r. + apply/seteqP; split => t /=. + rewrite /bigcap /= => /(_ (p @^-1` (ball (0 : R) r))). + by apply; rewrite inE. + by move => h; rewrite /bigcap /= => ?; rewrite inE => /eqP -> /=. + move => t /= [? ->] [y] bally <-; apply: pxrA => /=. + apply: le_lt_trans bally. + rewrite sub0r normrN [leRHS]ger0_norm ?norm_ge0//. + rewrite (le_trans (Theory.seminorm_normrB p _ _))//. + by rewrite opprD// addrA subrr add0r Theory.normN. +have nearp : (\forall y \near (nbhs x), -p(y - x) <= p(y) - p(x) <= p (y -x)). + apply: nearW => //= y. + by have := (Theory.seminorm_normrB p y x); rewrite ler_norml. +have lem : (p \o +%R^~ (- x)) x0 @[x0 --> nbhs x] --> (0 : R). + apply: (@cvg_comp _ _ _ (fun y => y - x) p); last first. + by rewrite -(@norm0 _ _ p); exact: continuous_at0_seminorm. + by rewrite -(subrr x)=> A /= /continuous_shift; apply. +apply: (@squeeze_cvgr _ (nbhs x)) => /=; first exact: nearp. + by rewrite -oppr0; apply: (@cvgN _ R^o); exact: lem. +exact: lem. +Qed. + +End convex_topology_seminorm. + +Section generating_seminorm. +Context {R : realType} {E : convexTvsType R}. + +Definition gauge_fun_basis (b : set E) (h : open_nbhsbasis_convextvs b) := + gauge_fun (open_absconvex_opennbhsbasis h).2 (absorbing_opennbhsbasis h). + +Definition seminorm_of := [set p : SemiNorm.type E | + exists b, exists h : open_nbhsbasis_convextvs b, p = gauge_fun_basis h]. + +#[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. +Proof. +have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E; move=> [/= b Bb _]. +exists (gauge_fun_basis Bb). +by exists b; exists Bb. +Qed. + +#[local] Notation seminormE := + (@seminorm_on R E seminorm_of seminorm_ofneq0 : convexTvsType R). + +Let ball_gauge_fun (A : set E) (r : R) (r0 : 0 < r) + (absA : absolutely_convex_set A) (pabsA : absorbing_set A) (_ : open A) : + (gauge_fun absA pabsA) @^-1` ball (0 : R) r = + (fun y : E => r^-1 *: y) @^-1` A. +Proof. +apply/seteqP; split => y /=; rewrite /ball /= sub0r normrN ger0_norm ?gauge_ge0//. + move/inf_lt => []. + have := pabsA y => -[r' r'0]; rewrite inE => r'yb. + exists r'^-1 => /=; split; first by rewrite invr_gt0. + rewrite inE /=; exists (r' *: y) => //. + by rewrite scalerA mulVf ?scale1r ?gt_eqF. + move=> t [t0]; rewrite inE => /= -[y' by' <-] tr. + have [_ /(_ (t / r))] := absA; apply. + by rewrite gtr0_norm ?divr_gt0// ler_pdivrMr// mul1r ltW. + by exists y' => //; rewrite scalerA mulrC. +move=> Ary. +have : exists2 t : R , (0 < t < 1) & (r^-1 *: y \in ( *:%R t ) @` A). + have /scalerx_continuous : nbhs (1 *: (r^-1 *: y)) A. + by rewrite scale1r; exact: open_nbhs_nbhs. + move => [s /= s0] b1s. + have ? : 0 < `|s| / 2 by rewrite divr_gt0 ?normr_gt0 ?gt_eqF. + exists ((1 + `|s| / 2)^-1). + by rewrite invr_gt0//= addr_gt0//= invf_lt1// ltrDl//. + rewrite inE; exists ((1 + `|s| / 2) *: (r^-1 *: y)). + apply: b1s => /=. + rewrite opprD addrA subrr sub0r normrN gtr0_norm// gtr0_norm// gtr_pMr//. + by rewrite invf_lt1// ltr1n. + by rewrite scalerA mulVf ?scale1r. +move=> [t /andP [t0 t1] rytb]. +have lepr : - (t * r) <= sup (-%R @` [set s | 0 < s /\ y \in ( *:%R s ) @` A]). + set B := (X in _ <= sup X). + have Br : B (- (t * r)). + exists (t * r); split => //; first by rewrite mulr_gt0. + rewrite inE; exists (t^-1 *: (r^-1 *: y)). + have := rytb; rewrite inE => -[z bz <-]. + by rewrite scalerA mulVf ?gt_eqF// scale1r. + by rewrite (scalerA t^-1) -invfM scalerA divff ?scale1r// gt_eqF// mulr_gt0. + have: has_ubound B by exists 0 => ? [s [s0 _]] <-; rewrite ltW // oppr_lt0. + by move/ub_le_sup/(_ _ Br). +apply: le_lt_trans; first by rewrite lerNl; exact lepr. +by rewrite gtr_pMl. +Qed. + +Theorem seminorm_convextvs : + continuous (id : E -> seminormE) /\ (continuous (id : seminormE -> E)). +Proof. +pose B := open_nbhsbasis_convextvs. +split=> x a. + move=> [/=b [?]] [I /= Ig] /= <- <- /filterS; apply. + apply/nbhs_add1set. + apply: filter_bigI => /= i /Ig /set_mem /= => -[? [b' [nb']]] -> [/= r r0 ->]. + have [/(_ b' nb') nbhsB _] := basis_opennbhsbasis E. + set p := (X in nbhs 0 (X @^-1` ball 0 r)). + have -> : p @^-1` ball (0 : R) r = (fun y : E => r^-1 *: y) @^-1` b'. + by apply: ball_gauge_fun => //; exact: (open_absconvex_opennbhsbasis nb').1. + by apply: scalexr_continuous; rewrite scaler0. +move => /nbhsE0 /= [ax] /= [b n0b ba]. +have [_ /(_ b n0b) /= [b'/=]] := basis_opennbhsbasis E. +move=> Bb' bb'. +pose p := gauge_fun (open_absconvex_opennbhsbasis Bb').2 + (absorbing_opennbhsbasis Bb'). +have /open_absconvex_opennbhsbasis [ob' absconvb'] := Bb'. +exists ([set x] `+ p @^-1` ball (0 : R) 1) => /=; last first. + rewrite ball_gauge_fun => // z/= [? ->] [y]; rewrite invr1 scale1r => b1y xyz. + by apply: ba; exists y => //; exact: bb'. +exists (p @^-1` ball (0 : R) 1) => //. +exists [fset p @^-1` (ball (0 : R) 1)]%fset. + move=> c; rewrite 2!inE => /eqP => ->. + exists p; last by exists 1. + by exists b', Bb'. +rewrite /bigcap; apply/seteqP; split => z /=. + by move => /(_ (p @^-1` ball (0: R) 1)); apply; rewrite inE. +by move => b1z ?; rewrite inE => /eqP ->. +Qed. + +Lemma continuous_seminorm_of q : seminorm_of q -> continuous q. +Proof. +have -> : (q : E -> R) = (q : seminormE -> R^o) \o (id : seminormE -> E) by []. +move=> qs x. +have contid : {for x, continuous (id : E -> seminormE)}. + by have [contid' _] := seminorm_convextvs; exact: contid'. +have cq : {for x, continuous (q : seminormE -> R^o)}. + exact: (@continuous_seminorm R^o E seminorm_of _ (id x)). +exact: (continuous_comp contid cq). +Qed. + +#[local] Definition cst0 : E -> R := fun x => 0. +#[local] Lemma cst00 : cst0 0 = 0. Proof. by []. Qed. +#[local] Lemma cst0_ge0 x : 0 <= cst0 x. Proof. by []. Qed. +#[local] Lemma ler_cst0D x y : cst0 (x + y) <= cst0 x + cst0 y. +Proof. by rewrite addr0. Qed. +#[local] Lemma cst0Z r x : cst0 (r *: x) = `|r| * cst0 x. +Proof. by rewrite mulr0. Qed. + +HB.instance Definition _ := @isSemiNorm.Build R E cst0 cst00 cst0_ge0 ler_cst0D cst0Z. + +(**md The literature usually states the following lemmas using a family of + seminorms $p_i$, a family of multiplicative constants $C_i$ and bounds the + absolute value of $l$ : `` `|l i| <= sup C_i p_i (x) ``. + We simplify these arguments using the linearity of $l$ to get rid of the + absolute value. *) +Lemma linear_continuous_seminorm (l : {scalar E}) : + continuous l -> + exists2 p : SemiNorm.type E, (seminorm_of p /\ continuous p) & + (forall x, l x <= p x). +Proof. +have [Bnbhs Bbasis] := basis_opennbhsbasis E. +move=> /[dup] cl /(_ 0 (ball (0 : R) 1)); rewrite linear0. +move=> /(_ (nbhsx_ballx (0 : R) 1 ltr01)). +have : 2^-1 !=0 :> R by []. +move/nbhsZ => /[apply]; rewrite scaler0 => /Bbasis /= [b /= Bb bl]. +have {}bl : b `<=` [set t | `|l t| < 2^-1]. + move => t /bl; rewrite /ball /= => -[x]; rewrite sub0r normrN. + by move=> lx <-; rewrite linearZ/= normrM ger0_norm// gtr_pMr. +have [_ /(_ 0 b (Bnbhs b Bb))] := seminorm_convextvs. +move=> n0b. +pose q : SemiNorm.type E := gauge_fun_basis Bb. +exists q. + split; first by exists b, Bb. + by apply: continuous_seminorm_of; exists b, Bb. +move => x. +have [->|x0] := eqVneq x 0; first by rewrite linear0 norm0. +have [qx0|qx0] := eqVneq (q x) 0. + (* case forgotten in the literature *) + suff: l x = 0 by move => ->; rewrite norm_ge0. + rewrite /q /= /gauge_fun /= in qx0. + have lxe (e : R) (e0 : 0 < e) : `|l x | < e. + have:= bl (e^-1 *: x) => /=. + rewrite linearZ /= normrM normfV ltr_pdivrMl ?normr_gt0 ?lt0r_neq0 //. + rewrite (gtr0_norm e0) => lem; apply : lt_trans. + apply: lem. + have hasinf : has_inf [set r | 0 < r /\ x \in ( *:%R r) @` b]. + split; last by exists 0 => z /= [] z0 _; apply: ltW. + have [r r0] := absorbing_opennbhsbasis Bb x. + move/set_mem => bx. + exists r^-1 => /=; split; rewrite ?invr_gt0 //; apply/mem_set. + by exists (r *: x) => //; rewrite scalerA ?mulVf ?lt0r_neq0 ?scale1r. + have [eps [eps0 /set_mem /= [y by' epsyx]]] := inf_adherent e0 hasinf. + rewrite qx0 add0r -epsyx scalerA => epse; rewrite ?mulVf. + have /(_ (e^-1 * eps)):= ((open_absconvex_opennbhsbasis Bb).2).2. + apply => //=; last by exists y. + by rewrite ger0_norm ?mulr_ge0 ?invr_ge0 ?ler_pdivrMl ?ltW ?mulr1. + by rewrite gtr_pMr ?invf_lt1 ?ltrDl //. + apply: contrapT => /eqP h. + have := lxe `|l x|. + by rewrite normr_gt0 h ltxx falseE; apply. +pose y := (2 * q x)^-1 *: x. +have : `|l y| < 2^-1. + apply/bl. + have : (q @^-1` ball (0 : R) 1) ((2 * q x)^-1 *: x). + move=> /=; rewrite sub0r normrN ger0_norm ?norm_ge0//. + rewrite normZ /= ger0_norm ?mulr_ge0 ?invr_ge0 ?norm_ge0//. + by rewrite mulr_ge0 ?norm_ge0 . + by rewrite invfM -mulrA mulVf// ltr_pdivrMl ?mulr1 ?ltrDl//= ltr01. + rewrite ball_gauge_fun => //; first by have [] := open_absconvex_opennbhsbasis Bb. + by rewrite /= invr1 scale1r. +rewrite /y linearZ normrM normfV normrM ger0_norm// ltr_pdivrMl. + by rewrite mulr_gt0 ?normr_gt0. +rewrite mulrAC divff ?mul1r// [in X in _ < X -> _]ger0_norm ?norm_ge0//. +by move/ltW; apply: le_trans; exact: ler_norm. +Qed. + +Lemma linear_seminorm_continuous (l : {scalar E}) : + (exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x)) -> + continuous (l : E -> R^o). +Proof. +move=> [p px lpxl]; apply: continuousfor0_continuous => /= a. +rewrite linear0 => -[/= e e0] balla. +have /filterS : p @^-1` (ball_ normr 0 e) `<=` l @^-1` a. + move=> z /=; rewrite sub0r normrN ger0_norm ?norm_ge0// => pze. + apply: balla => /=; rewrite sub0r normrN. + apply: le_lt_trans pze. + have [g0|g0] := leP 0 (l z); first by rewrite ger0_norm. + rewrite ltr0_norm//; have := lpxl (- z). + by rewrite linearN -[in X in _ <= X -> _]scaleN1r normZ normrN1 mul1r. +apply => /=; rewrite -(@norm0 _ _ p); apply: px. +by rewrite norm0 ; apply: nbhsx_ballx. +Qed. + +Proposition lcfun_seminorm (l : {scalar E}) : + continuous l <-> + exists2 p : SemiNorm.type E, continuous p & (forall x, l x <= p x). +Proof. +split; last exact: linear_seminorm_continuous. +by move/linear_continuous_seminorm => [p [_ cp] lpx]; exists p. +Qed. + +End generating_seminorm. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index ad27fb5a56..c9d2d88948 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order algebra all_classical. +From mathcomp Require Import boot order algebra all_classical finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. @@ -101,6 +101,12 @@ rewrite nbhs_filterE; apply: filterS FC. by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image. Qed. +Lemma initial_nbhs_preimage (w : W) A : nbhs (f w) A -> nbhs w (f @^-1` A). +Proof. +rewrite nbhsE /= => -[B [oB Bfx]] BA. +by exists (f @^-1` B); split => //= ; [exists B|move=> z /= /BA]. +Qed. + End Initial_Topology. (*#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed `initial_open`")] Notation wopen := initial_open (only parsing).*) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 664ab142f5..e1607edf91 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -560,6 +560,13 @@ HB.instance Definition _ := Nbhs_isTopological.Build T HB.end. +Definition openU_from (T : Type) (I : Type) (D : set I) (b : I -> set T) := + [set \bigcup_(i in D') b i | D' in subset^~ D]. + +#[deprecated(since="mathcomp-analysis 1.17.0", use=openU_from)] +Notation open_from := openU_from (only parsing). + + (** Topology defined by a base of open sets *) HB.factory Record isBaseTopological T & Choice T := { @@ -571,9 +578,6 @@ HB.factory Record isBaseTopological T & Choice T := { exists k, [/\ D k, b k t & b k `<=` b i `&` b j] }. -Definition openU_from T I (D : set I) (b : I -> set T) := - [set \bigcup_(i in D') b i | D' in subset^~ D]. - HB.builders Context T & isBaseTopological T. Local Notation openU_from := (openU_from D b). @@ -623,8 +627,6 @@ HB.instance Definition _ := isOpenTopological.Build T HB.end. -#[deprecated(since="mathcomp-analysis 1.17.0", use=openU_from)] -Notation open_from := openU_from (only parsing). HB.factory Record isSubBaseTopological T & Choice T := { I : pointedType ; @@ -1119,6 +1121,9 @@ Context {T : topologicalType}. Definition basis (B : set_system T) := B `<=` open /\ forall x : T, filter_from [set U | B U /\ U x] id --> x. +Definition nbhs_basis (x : T) (B : set (set T)) := + B `<=` nbhs x /\ filter_from [set U | B U] id --> x. + Definition separable_set (A : set T) := exists D, [/\ countable D, D `<=` A & forall O, A `&` O !=set0 -> open O -> O `&` D !=set0]. From a4cab893606ddd306a63f70234fc61680a2d85d0 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Tue, 7 Jul 2026 16:07:13 +0900 Subject: [PATCH 2/3] haussdorf ctvs --- .../functional_analysis/hahn_banach_theorem.v | 108 +++++++ theories/normedtype_theory/tvs.v | 296 +++++++++++++++++- 2 files changed, 403 insertions(+), 1 deletion(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 378d8e7bc3..2d0e250d45 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -367,6 +367,39 @@ Qed. End hahn_banach_normed. + + +Section line_lmodtype. +Variable (R : numDomainType) (V: lmodType R) (x : V). + +Definition linepred : {pred V} := mem [set y | exists t, y = t *: x ]. +Definition line := {y | linepred y}. + +Lemma line_linepred (y : line) : exists t, val(y) == t *: x. +Proof. +by move: y => [yv] /= /asboolP [t] ->; exists t. +Qed. + + +#[local] Lemma line_submod_closed : submod_closed (linepred). +Proof. +split; first by rewrite inE; exists 0; rewrite scale0r. +move=> t y z; rewrite !inE => -[ty ->] -[tz ->]; exists (t * ty + tz). +by rewrite scalerDl scalerA. +Qed. + +HB.instance Definition _ := + @GRing.isSubmodClosed.Build _ _ linepred line_submod_closed. + + +HB.instance Definition _ := SubChoice.on line. + +HB.instance Definition _ := [SubChoice_isSubLmodule of line by <:]. + +Check (line : lmodType R). +Check (line : subLmodType linepred). +End line_lmodtype. + Section hahn_banach_extension_ctvs. Context {R : realType} {V : convexTvsType R} (F : pred V). (**md Contrary to the normed case, the extension theorem is not true for any @@ -457,3 +490,78 @@ by exists g'. Qed. End hahn_banach_extension_ctvs. + +Check scalerI. +Check scaler_injl. + +(* TBA : to classical *) +Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : a != 0 -> (t *: a = 0 -> t = 0). +Proof. +move=> a0 ta; apply: contrapT => /eqP t0. +have : t^-1 *: (t *: a) = 0 by rewrite ta scaler0. +by rewrite scalerA mulVf// scale1r; apply/eqP. +Qed. + +Lemma scaleIl (R : numFieldType) (V: lmodType R) (a : V) : a != 0 -> injective (fun t => t *: a). +Proof. +move=> a0 s t => /eqP; rewrite -subr_eq0 -scalerBl => /eqP /(scaler_eq0 a0) /eqP. +by rewrite subr_eq0 => /eqP. +Qed. +(*END TBA *) + +(* 7.2.3 in Jarchow *) +Lemma hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) : +(hausdorff_space V) <-> (forall x : V, x != 0 -> exists l : {linear_continuous V -> R^o}, l(x) != 0). +Proof. +split; last first. +(* proof in here is different than in the book - Jarchow mentions "a" continuous seminorm in 7.2.3 but refers to 2.7.1 which proves the results for a seminorm of the set of seminorm generating the topology - its probably lacks an argument saying that continuous seminorms are always bounded by this set of seminorms, which we haven't formalised here *) + move => H. + pose P := (@seminorm_of R V). + pose P0 := (@seminorm_ofneq0 R V). + suff : hausdorff_space (seminorm_on P0). + have [contVs _ ] := (seminorm_convextvs V). + by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; apply: cs => //. + apply/hausdorff_seminorm_on=> x /H [l]. + have [l0|l0|] := ltrgtP (l x) (0 : R) => //. + have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ (-1 *: l)). + exists p => //; apply: lt_le_trans; last by apply: lp. + by rewrite scaleN1r ltrNr oppr0. + have /linear_continuous_seminorm [p [sp _] /= lp] := (@continuous_fun _ _ l). + by exists p => //; apply: lt_le_trans; last by apply: lp. +move=> haus x x0. +pose l := fun ( y : line x) => xchoose (line_linepred y). +have llinear: linear_for ( *:%R) l. + rewrite /l /= => t /= u v; apply: scaleIl; first by exact: x0. + rewrite scalerDl -scalerA. + move/eqP: (xchooseP (line_linepred u)) => <-. + move/eqP: (xchooseP (line_linepred v)) => <-. + move/eqP: (xchooseP (line_linepred (t *: u + v))) => <-. + by rewrite (@GRing.valD _ _ (line x)) (*why is it necessary to have the @? *) GRing.valZ. +pose linlP := GRing.isLinear.Build _ _ _ _ l llinear. +pose linl : {linear ((init_subconvextvs (line x))) -> R^o} := HB.pack l linlP. +have lcont : continuous linl. + apply/continuous_closedkernel. + have -> : (linl @^-1` [set 0]) = [set 0]. + apply/seteqP; split => u /=. + move/eqP: (xchooseP (line_linepred u)) => /[swap]; rewrite /l => ->. + by rewrite scale0r -(@GRing.val0 _ _ (line x)) => /val_inj. + move=> u0; move/eqP: (xchooseP (line_linepred u)). + rewrite u0 /= /l; move/eqP; rewrite eq_sym => /eqP. + by move/(scaler_eq0 x0). + apply: accessible_closed_set1; apply: hausdorff_accessible. + by apply: hausdorff_init_convextvs. +pose contlP := isContinuous.Build _ _ _ lcont. +pose lcl : {linear_continuous (init_subconvextvs (line x)) -> R^o} := + HB.pack (l : (init_subconvextvs (line x)) -> R^o) linlP contlP. +have := (hahn_banach_extension_initialsubctvs lcl) => -[g Pg]; exists g. +have xlinepred : (linepred x) x by apply/asboolP; exists 1; rewrite scale1r. +pose xline := exist (linepred x) _ xlinepred;have <- : \val xline = x by []. +rewrite Pg. +suff -> : lcl xline = 1 by []. +move/eqP: (xchooseP (line_linepred xline)). +set xline':= (X in X =_ -> _); have -> : xline' = x by []. (*weakness of line, to be understood *) +set x':= (X in X =_ -> _); rewrite -(scale1r x'). +move/scaleIl => H; apply/eqP; rewrite eq_sym; apply/eqP. +by apply: H. +Qed. +(* TODO : more hahn banach separation theorems *) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 8b3f88c1b5..8618b404a3 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -8,6 +8,7 @@ From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import convex set_interval reals topology. From mathcomp Require Import initial_topology num_normedtype. From mathcomp Require Import pseudometric_normed_Zmodule. +From mathcomp Require Import contra. (**md**************************************************************************) (* # Topological vector spaces *) @@ -203,6 +204,16 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. + +Lemma accessible_field (K : numFieldType) : accessible_space K^o. +Proof. +move=> x y xy. +exists (ball x (`|x-y|/2)); split; rewrite ?inE /=; first by apply: ball_open. + by apply: ballxx; rewrite mulr_gt0 ?normr_gt0 ?invr_gt0 ?subr_eq0. +rewrite /ball /= ltr_pdivlMr //= gtr_pMr ?normr_gt0 ?subr_eq0 //. +by rewrite ltrn1. +Qed. + Section TopologicalLmodule_theory. Context {R : numFieldType} (E : topologicalLmodType R). @@ -218,6 +229,7 @@ Lemma fun_cvgZr (T : Type) (U : set_system T) {FF : Filter U} k (f : T -> E) a : f @ U --> a -> k \*: f @ U --> k *: a. Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. + Lemma nbhs0Z (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. @@ -235,6 +247,50 @@ 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. +Lemma continuousfor0_continuous (f : {linear F -> G}) : + {for 0, continuous f} -> continuous f. +Proof. +move=> cont0 x. +suff: (f y - f x)@[y --> x] --> (0 : G). + have -> : (fun y : F => f y - f x) = (fun y : F => f (y - x) : G). + by apply: funext => y; rewrite linearB. + move=> fxfy /= A nA /=. + pose B := [set y - f x | y in A]. + have /fxfy : nbhs 0 B. + have -> : B = (+%R^~ (- (- f x))) @^-1` A. + rewrite opprK; apply/seteqP; split. + by move=> y [/= g Ag <-]; rewrite subrK. + move=> g/= Agfx; eexists; first exact: Agfx. + by rewrite addrK. + have:= @continuous_shift _ (0 : G) (f x) A. + by rewrite opprK add0r => /(_ nA); exact. + rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=. + by move=> [y Ay]; rewrite linearB => /subIr <-. +have -> : (fun y => f y - f x) = (fun y => f (y - x)). + by apply: funext => y; rewrite linearB. +apply: cvg_comp; last by rewrite -(linear0 f); exact: cont0. +by move => A nA /=; apply: continuous_shift; rewrite subrr. +Qed. + +Lemma hausdorff_convextvs : (hausdorff_space F) <-> closed ([set 0 : F]). +Proof. +split. + move=> /(_ (0:F)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. + move=> a b n0a /(cl b) [? [-> b0]]. + exists 0; split => //; exact: nbhs_singleton. +move => cl. +(* simpler proof using the closed subbasis ?*) +move=> x y H; apply: subr0_eq; have := H. +contra => xy0. +have nxy : nbhs (x-y) (~`[set 0]). + apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. + by apply/eqP. +have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). + by exact: sub_continuous. +move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. +by have := ab0 (z,z) => /=; rewrite subrr; apply. +Qed. + End TopologicalLmodule_theory. Section TopologicalLmodule_numDomain. @@ -507,6 +563,21 @@ HB.instance Definition _ := @Uniform_isConvexTvs.Build R init_subconvextvs locally_convex_sub. HB.instance Definition _ := GRing.SubLmodule.on init_subconvextvs. +Lemma hausdorff_init_convextvs : hausdorff_space V -> hausdorff_space init_subconvextvs. +Proof. +move=> hV x y; +rewrite /cluster /= /nbhs /= => cl. +apply: val_inj; apply: hV; rewrite nbhsE => A B /= [A' [oA Ax AA']]. +rewrite nbhsE /= => -[B' [oB By BB']]. +have valA: nbhs_of_open (initial_open \val) x (\val @^-1` A'). + by rewrite /nbhs_of_open; exists (\val @^-1` A'); split => //=; exists A'. +have : nbhs_of_open (initial_open \val) y (\val @^-1` B'). + by rewrite /nbhs_of_open; exists (\val @^-1` B'); split => //=; exists B'. +move/(cl (val @^-1` A') (val @^-1` B') valA) => [z /= [Az Bz]]; exists (val z); split. + by apply: AA'. +by apply: BB'. +Qed. + End SubLmodule_isSubConvexTvs. HB.factory Record PreTopologicalLmod_isConvexTvs (R : numDomainType) E @@ -658,6 +729,7 @@ HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. HB.end. + HB.factory Record NbhsBasisAt0_isConvexTvs (R : numFieldType) E & GRing.Lmodule R E := { nbhsbasis_at0 : set_system E ; @@ -939,6 +1011,32 @@ HB.end. Section ConvexTvs_realType. +End ConvexTvs_realType. + + +Section ConvexTvs_realType. + +(*better naming ?*) +Lemma scalerx_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : + {for s, continuous (fun t : R^o => t *: x)}. +Proof. +have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)). + exact: funext. +apply: continuous_comp. +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. +exact: (scale_continuous (s, x)). +Qed. + +Lemma scalexr_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : + {for x, continuous (fun y : E => s *: y)}. +Proof. +have -> : (fun y : E => s *: y) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). + exact: funext. +apply: continuous_comp. +apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. +exact: (scale_continuous (s, x)). +Qed. + End ConvexTvs_realType. Section standard_topology. @@ -1265,6 +1363,79 @@ Qed. End openbasis. + +Section closedbasis. +Context (R : realFieldType) (E: convexTvsType R). + +Definition closed_nbhsbasis_ctvs := [set closure b | b in (@nbhsbasis_convextvs R E)]. + +(* TODO : convex is enough and then take balanced closure *) + +Lemma closure_convextvs ( b : set E) : + closure b = \bigcap_(a in (nbhs (0 : E))) (b `+ a). +Proof. +have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +apply/seteqP; split => z H. + move=> a' /basis [/=a /[dup] /mem_set /absconv [_ bala]]. + move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. + exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. + by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. +move=> d; rewrite nbhsE0=> -[c /basis [/=a /[dup] /mem_set /absconv [_ bala]]]. +move=> /nbhs0 /H [x bx [y ay]] xyz ac zcd. +exists x; split => //; apply: zcd; exists (-y). + by rewrite -scaleN1r; apply/ac/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. +by apply: (addrI y); rewrite addrCA subrr addr0 addrC. +Qed. + +Lemma closure_addsetset (b : set E) : (nbhs 0 b) -> closure b `<=` b `+ b. +Proof. +move=> nb z. rewrite closure_convextvs /bigcap /= => /(_ b nb) [x bx [y by' <-]]. +by exists x => //; exists y. +Qed. + +Lemma has_closed_nbhs_basis : + nbhs_basis 0 closed_nbhsbasis_ctvs + /\ (forall b, closed_nbhsbasis_ctvs b -> (closed b /\ absolutely_convex_set b)). +Proof. +have [absconv [] nbhs0 basis] := (svalP (cid2 (@locally_convex _ E))). +split. + split; move=> /= a /=. + by move=> [b /nbhs0 nbhsb <-]; apply: filterS; first by apply: subset_closure. + move=> /nbhs0_add [b] /[dup] /basis [/= c nc cb]. + move=> /closure_addsetset /subset_trans /[apply] cba. + exists (closure c); first by exists c. + apply: subset_trans; last by exact: cba. + by apply: closureS. +move=> ? [c nc <-]; split; first by exact: closed_closure. +have [convc balc] := absconv c (mem_set nc). +split; rewrite /closure. + move => x y t; rewrite !inE /= => Bx By B. + move/nbhsE0 => [a /basis [/= a' na' aa'] aB]. + have [conva _] := absconv a' (mem_set na'). + have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a') !=set0. + apply: (Bx ([set x] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + by move=> z /= [s sa <-]; exists x => //; exists s. + have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a') !=set0. + apply: (By ([set y] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + by move=> // z /= [s sa <-]; exists y => //; exists s. + exists (conv t (cx : convex_lmodType E) cy); split. + by apply/set_mem; apply: convc; rewrite !inE. + apply: aB => /=; rewrite -acy -acx; exists (conv t (ax : convex_lmodType E) ay). + by apply: aa'; apply/set_mem; apply: conva; rewrite !inE. + by rewrite addrACA -!scalerDr. +move=> t t1 ? /= [x Bx] <- B. +have [->|t0] := eqVneq t 0. + by rewrite scale0r => /nbhs_singleton B0; exists 0; split => //; apply: nbhs_singleton; apply: nbhs0. +move/(nbhsZ (invr_neq0 t0)); rewrite scalerA mulrC divff // scale1r. +move/Bx => [z [cz [y by']]] /(congr1 (fun x => t *: x)). +rewrite scalerA divff // scale1r => ytz; exists y; split => //. +rewrite ytz; apply: balc; first by exact: t1. +by exists z. +Qed. + +End closedbasis. + + Import Norm. Definition gauge_fun (K : realType) (V : lmodType K) (A : set V) @@ -1344,7 +1515,6 @@ rewrite !inE => /(_ Av Aw); rewrite /conv /=; apply. by rewrite !scalerA divff ?scale1r //; rewrite gt_eqF // addr_gt0. Qed. - #[local] Lemma gaugeZ r v : gauge_fun (r *: v) = `|r| * gauge_fun v. Proof. rewrite /gauge_fun; have [->|] := eqVneq r 0. @@ -1386,6 +1556,7 @@ End gauge. Definition seminorm_on {R : realFieldType} {E : lmodType R} (P : set (SemiNorm.type E)) (Hp : P !=set0) : Type := E. + Section convex_topology_seminorm. Context (R : realFieldType) (E : lmodType R) (P : set (SemiNorm.type E)) (H : P !=set0). @@ -1545,6 +1716,39 @@ apply: (@squeeze_cvgr _ (nbhs x)) => /=; first exact: nearp. exact: lem. Qed. + +Lemma hausdorff_seminorm_on : +hausdorff_space (seminorm_on H) <-> (forall x : E, x != 0 -> exists2 p, P p & 0 < p x). +Proof. +split. + move/hausdorff_convextvs => P0 x; contra => HP. + have : forall p, P p -> p x = 0. + move=> p /HP /negP nlt0. + have:= (@norm_ge0 _ _ p x). + rewrite le0r; case; move/orP => []; first by move/eqP. + by move/nlt0 => //. + move => {HP} HP; apply: P0 => /= c [? [?]] [/= I IB] <- <- xic. + exists 0; split => //; apply: xic => /=; exists x => //; exists (-x); rewrite ?subrr //. + move=> i /= /IB /set_mem /= [p] /HP px0 [e e0] -> /=. + rewrite Theory.normN px0. + by apply: ballxx. +move=> P0; apply/hausdorff_convextvs => x /=; contra => /P0 [p Pp px0]. +exists (p @^-1` ball (p x) (p x)); last first. + by move=> /= ? ->; rewrite norm0 /ball /= subr0 ger0_norm ?norm_ge0 // ltxx. +exists ([set x] `+ p @^-1` ball (0 : R) (p x)); last first. + move=> z /= [? -> [y + <-]]. + rewrite /ball /= sub0r normrN ger0_norm ?norm_ge0 // => pyx. + apply: le_lt_trans; first by apply: Theory.seminorm_normrB. + by rewrite opprD addrA subrr sub0r Theory.normN. +exists (p @^-1` ball (0 : R) (p x)) => //. +exists ([fset (p @^-1` ball (0 : R) (p x))]%fset). + move=> ? ; rewrite inE => /eqP ->; apply/mem_set. + rewrite /seminorm_subbasis /=; exists p => //; exists (p x) => //. +apply/seteqP; split => z /=. + by rewrite /bigcap /= => /(_ (p @^-1` ball (0 : R) (p x))); apply; rewrite inE. +by move=> ballz => ? /=; rewrite inE => /eqP ->. +Qed. + End convex_topology_seminorm. Section generating_seminorm. @@ -1556,6 +1760,7 @@ Definition gauge_fun_basis (b : set E) (h : open_nbhsbasis_convextvs b) := Definition seminorm_of := [set p : SemiNorm.type E | exists b, exists h : open_nbhsbasis_convextvs b, p = gauge_fun_basis h]. + #[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E; move=> [/= b Bb _]. @@ -1754,3 +1959,92 @@ by move/linear_continuous_seminorm => [p [_ cp] lpx]; exists p. Qed. End generating_seminorm. + + +Section kernel. +Context (R : realFieldType) (F : convexTvsType R). +(* Necessary to use has_open_nbhs_basis *) + +(*TBA topology *) +Lemma closed_Ndense (S : set F) : (S != [set: F]) -> closed S -> ~ (dense S). +Proof. +move=> /setTPn [t] nSt. +have S0: (~` S) !=set0 by exists t. +rewrite -openC => /[swap] /(_ _) /[swap] oS /(_ (~` S) S0 oS). +by move=> -[a [+ Sa]]; move=> /(_ Sa). +Qed. + +(* Introduce a notation for kernels ?*) +Lemma continuous_closedkernel (f : {linear F -> R^o}): continuous f <-> closed (f @^-1` [set 0]). +Proof. +split. + move=> /continuous_closedP /(_ [set 0]); apply. + apply: accessible_closed_set1; apply: accessible_field. +have []:= (eqVneq (f @^-1` [set 0]) [set : F]). + move => h _. + suff -> : f = (fun y=> 0) :> (F -> R) by apply: cst_continuous. + apply: funext => x. + have : [set : F] x by []. + by rewrite -h /=. +move=> s0 /closed_Ndense; move=> /(_ s0). +move=> /existsNP [U] /not_implyP [[x Ux]]. +move=> /not_implyP [oU] /forallNP /= Uf. +have [B Bconv [B0 Bbasis]] := (@locally_convex _ F). +have /nbhsE0 [V' /Bbasis [/= V BV VV'] VU]: nbhs x U by rewrite nbhsE; exists U. +have [_ aV]: absolutely_convex_set V by apply: Bconv; rewrite inE. +have nfU: forall z, V z -> f z != f x. + move=> z Vz; apply/eqP => fzx. + have Vnz : V (- z). + rewrite -scaleN1r; apply: aV; last by exists z => //. + by rewrite normrN normr1. + apply: Uf; split; first by apply: VU ; exists (-z); first by apply: VV'. + by rewrite linearB; rewrite fzx subrr. +have [/=M fM]: exists M, forall z, V z -> `|f z | < M. + apply: contrapT; rewrite -forallNE /= => /(_ (`|f x|)) /existsNP [y]. + move=> /not_implyP [Vy] /negP; rewrite -leNgt => fxy. + have fy0 : f y != 0. + apply/eqP => fy0; move: fxy; rewrite fy0 normr0 normr_le0 => /eqP fx0. + by apply: (Uf x); split. + have Vyx : V ((`| f x|/ `| f y|) *: y). + apply: aV; last by exists y. + rewrite ger0_norm ?mulr_ge0 ?invr_ge0 //. + rewrite ler_pdivrMr ?mul1r // normr_gt0; apply/eqP => fy. + have := fxy; rewrite fy normr0 normr_le0 => /eqP fx0. + by apply: (Uf x); split. + have Vnyx : V ( - (`| f x|/ `| f y|) *: y). + apply: aV; last by exists ((`| f x|/ `| f y|) *: y); rewrite // scalerA -mulN1r. + by rewrite normrN normr1. + have [] := ltgtP 0 ((f x)/(f y)). + - move=> fxy0. + apply: (Uf ( x - (`|f x| / `|f y|) *: y)); split. + apply: VU; exists (- (`|f x| / `|f y|) *: y); first by apply: VV'. + by rewrite scaleNr. + rewrite linearD linearN linearZ /=. + have -> : `|f x| / `|f y| = (f x)/(f y) by rewrite -normfV -normrM gtr0_norm. + by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. + - move=> fxy0. + apply: (Uf ( x + (`|f x| / `|f y|) *: y)); split. + by apply: VU; exists ((`|f x| / `|f y|) *: y); first by apply: VV'. + rewrite linearD linearZ /=. + have -> : `|f x| / `|f y| = - (f x)/(f y). + by rewrite -normfV -normrM ltr0_norm ?mulNr. + by rewrite -[_ *: _]/(_ * _) -mulrA mulVf ?mulr1 ?subrr. + - move=> /eqP; rewrite eq_sym mulf_eq0 => /orP [] /eqP. + by move=> fx0; apply: (Uf x); split. + by rewrite -invr0 => /invr_inj fyn0; move/eqP: fy0; apply. +have [M0|M0] := leP M 0 => //. + have := (fM 0); move => /(_ (nbhs_singleton _)); move=> /(_ (B0 V BV)). + by move=> /lt_le_trans /(_ M0); rewrite normr_lt0. +apply: continuousfor0_continuous => /= A; rewrite linear0 => -[r /= r0] rA. +have rM0 : r/ M != 0 by apply: lt0r_neq0; rewrite ?mulr_gt0 ?invr_gt0 //. +apply: (@filterS _ _ _ ( *:%R (r * M^-1) @` V)); last first. + by rewrite -(@scaler0 _ _ (r/M)); apply: nbhsZ; last by apply: B0. +move=> z /= [t] Vt <-; rewrite linearE /=; apply: rA => /=. +rewrite sub0r normrN -[_ *: _]/(_ * _) normrM -ltr_pdivlMl. + by rewrite normr_gt0 //. +rewrite [in X in _ Date: Tue, 20 Oct 2026 22:12:52 +0200 Subject: [PATCH 3/3] fix rebase over seminorm --- .../functional_analysis/hahn_banach_theorem.v | 3 - .../pseudometric_normed_Zmodule.v | 30 ++++- theories/normedtype_theory/tvs.v | 110 ++++-------------- 3 files changed, 50 insertions(+), 93 deletions(-) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 2d0e250d45..1756ad2035 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -491,9 +491,6 @@ Qed. End hahn_banach_extension_ctvs. -Check scalerI. -Check scaler_injl. - (* TBA : to classical *) Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t : a != 0 -> (t *: a = 0 -> t = 0). Proof. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index eb070aab1b..4b0ff91793 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -6,7 +6,7 @@ From mathcomp Require Import interval interval_inference archimedean. From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import set_interval ereal reals topology. -From mathcomp Require Import num_normedtype. +From mathcomp Require Import num_normedtype contra. (**md**************************************************************************) (* # Normed topological abelian groups *) @@ -261,6 +261,34 @@ apply: funext => z /=; apply: propext; split=> [Az|[_ -> [y By]]]. by rewrite addrC => /addIr <-. Qed. +Lemma nbhs0_add (A : set M) : nbhs 0 A -> exists2 B, nbhs 0 B & B `+ B `<=` A. +Proof. +move=> na. +have := add_continuous 0 A. +rewrite add0r => /(_ na) /= -[[b1 b2] /= [n1 n2] ba]. +exists (b1 `&` b2); first by apply: filterI. +by move => z /= [x [x1 _]] [y [_ y2]] <-; apply (ba (x,y)); split => /=. +Qed. + +Lemma hausdorff_convextvs : (hausdorff_space M) <-> closed ([set 0 : M]). +Proof. +split. + move=> /(_ (0:M)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. + move=> a b n0a /(cl b) [? [-> b0]]. + exists 0; split => //; exact: nbhs_singleton. +move => cl. +(* simpler proof using the closed subbasis ?*) +move=> x y H; apply: subr0_eq; have := H. +contra => xy0. +have nxy : nbhs (x-y) (~`[set 0]). + apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. + by apply/eqP. +have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). + by exact: sub_continuous. +move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. +by have := ab0 (z,z) => /=; rewrite subrr; apply. +Qed. + End TopologicalZmoduleTheory. HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 8618b404a3..8c1fd821a2 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -214,6 +214,7 @@ rewrite /ball /= ltr_pdivlMr //= gtr_pMr ?normr_gt0 ?subr_eq0 //. by rewrite ltrn1. Qed. + Section TopologicalLmodule_theory. Context {R : numFieldType} (E : topologicalLmodType R). @@ -229,7 +230,6 @@ Lemma fun_cvgZr (T : Type) (U : set_system T) {FF : Filter U} k (f : T -> E) a : f @ U --> a -> k \*: f @ U --> k *: a. Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. - Lemma nbhs0Z (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. @@ -247,50 +247,6 @@ 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. -Lemma continuousfor0_continuous (f : {linear F -> G}) : - {for 0, continuous f} -> continuous f. -Proof. -move=> cont0 x. -suff: (f y - f x)@[y --> x] --> (0 : G). - have -> : (fun y : F => f y - f x) = (fun y : F => f (y - x) : G). - by apply: funext => y; rewrite linearB. - move=> fxfy /= A nA /=. - pose B := [set y - f x | y in A]. - have /fxfy : nbhs 0 B. - have -> : B = (+%R^~ (- (- f x))) @^-1` A. - rewrite opprK; apply/seteqP; split. - by move=> y [/= g Ag <-]; rewrite subrK. - move=> g/= Agfx; eexists; first exact: Agfx. - by rewrite addrK. - have:= @continuous_shift _ (0 : G) (f x) A. - by rewrite opprK add0r => /(_ nA); exact. - rewrite /nbhs /=; apply/filterS => z /=; rewrite /B /=. - by move=> [y Ay]; rewrite linearB => /subIr <-. -have -> : (fun y => f y - f x) = (fun y => f (y - x)). - by apply: funext => y; rewrite linearB. -apply: cvg_comp; last by rewrite -(linear0 f); exact: cont0. -by move => A nA /=; apply: continuous_shift; rewrite subrr. -Qed. - -Lemma hausdorff_convextvs : (hausdorff_space F) <-> closed ([set 0 : F]). -Proof. -split. - move=> /(_ (0:F)) hF x /= cl; apply/eqP; rewrite eq_sym; apply/eqP; apply: hF. - move=> a b n0a /(cl b) [? [-> b0]]. - exists 0; split => //; exact: nbhs_singleton. -move => cl. -(* simpler proof using the closed subbasis ?*) -move=> x y H; apply: subr0_eq; have := H. -contra => xy0. -have nxy : nbhs (x-y) (~`[set 0]). - apply: open_nbhs_nbhs; split => /=; first by apply: closed_openC. - by apply/eqP. -have /(_ (~`[set 0]) nxy) [] : continuous_at (x,y) (fun z => (z.1 - z.2)). - by exact: sub_continuous. -move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz. -by have := ab0 (z,z) => /=; rewrite subrr; apply. -Qed. - End TopologicalLmodule_theory. Section TopologicalLmodule_numDomain. @@ -1008,37 +964,6 @@ HB.instance Definition _ := @NbhsBasisAt0_isConvexTvs.Build R E HB.end. -Section ConvexTvs_realType. - - -End ConvexTvs_realType. - - -Section ConvexTvs_realType. - -(*better naming ?*) -Lemma scalerx_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : - {for s, continuous (fun t : R^o => t *: x)}. -Proof. -have -> : (fun t : R^o => t *: x) = (fun z => z.1 *: z.2) \o (fun r => (r,x)). - exact: funext. -apply: continuous_comp. -apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. -exact: (scale_continuous (s, x)). -Qed. - -Lemma scalexr_continuous (R : realFieldType) (E : convexTvsType R) (x : E) (s : R) : - {for x, continuous (fun y : E => s *: y)}. -Proof. -have -> : (fun y : E => s *: y) = (fun z => z.1 *: z.2) \o (fun y => (s, y)). - exact: funext. -apply: continuous_comp. -apply: (@cvg_pair _ _ _ _ (nbhs s)) => //=. -exact: (scale_continuous (s, x)). -Qed. - -End ConvexTvs_realType. - Section standard_topology. Context {R : numFieldType}. @@ -1296,7 +1221,7 @@ End lcfunproperties. Local Open Scope convex_scope. Section openbasis. -Context (R : realType) (E : convexTvsType R). +Context (R : realFieldType) (E : convexTvsType R). Definition nbhsbasis_convextvs := sval (cid2 (@locally_convex _ E)). @@ -1380,10 +1305,11 @@ apply/seteqP; split => z H. move=> /nbhs0 /[dup] na /(nbhs_add1set z)/H [y [by' [? -> [t ta zty]]]] aa'. exists y => //; exists (-t); last by apply: (addrI t); rewrite addrCA subrr addr0 addrC. by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists t. -move=> d; rewrite nbhsE0=> -[c /basis [/=a /[dup] /mem_set /absconv [_ bala]]]. -move=> /nbhs0 /H [x bx [y ay]] xyz ac zcd. +move=> d; rewrite nbhsE0. +move => [dz] [/=a /basis [ /= a'/[dup] /mem_set /= /absconv [_ bala]]]. +move=> /nbhs0 /H [x bx [y ay]] xyz aa' zcd. exists x; split => //; apply: zcd; exists (-y). - by rewrite -scaleN1r; apply/ac/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. + by rewrite -scaleN1r; apply/aa'/(bala (-1)); rewrite ?normrN ?normr1 //=; exists y. by apply: (addrI y); rewrite addrCA subrr addr0 addrC. Qed. @@ -1410,18 +1336,24 @@ move=> ? [c nc <-]; split; first by exact: closed_closure. have [convc balc] := absconv c (mem_set nc). split; rewrite /closure. move => x y t; rewrite !inE /= => Bx By B. - move/nbhsE0 => [a /basis [/= a' na' aa'] aB]. - have [conva _] := absconv a' (mem_set na'). - have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a') !=set0. - apply: (Bx ([set x] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + move/nbhsE0 => [Bxy [b /basis [/= a /[dup ]/nbhs0 na0 na ab] aB]]. + have [conva _] := absconv a (mem_set na). + have [cx [ccx [? /= -> [ax aax acx]]]] : c `&` ([set x] `+ a) !=set0. + apply: (Bx ([set x] `+ a)); rewrite nbhsE0; split. + exists x => //=; exists 0; last by rewrite addr0. + by apply: nbhs_singleton. + exists a; first by apply: nbhs0. by move=> z /= [s sa <-]; exists x => //; exists s. - have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a') !=set0. - apply: (By ([set y] `+ a')); rewrite nbhsE0; exists a'; first by apply: nbhs0. + have [cy [ccy [? /= -> [ay aay acy]]]] : c `&` ([set y] `+ a ) !=set0. + apply: (By ([set y] `+ a )); rewrite nbhsE0; split. + exists y => //=; exists 0; last by rewrite addr0. + by apply: nbhs_singleton => //=. + exists a ; first by apply: nbhs0. by move=> // z /= [s sa <-]; exists y => //; exists s. exists (conv t (cx : convex_lmodType E) cy); split. by apply/set_mem; apply: convc; rewrite !inE. apply: aB => /=; rewrite -acy -acx; exists (conv t (ax : convex_lmodType E) ay). - by apply: aa'; apply/set_mem; apply: conva; rewrite !inE. + by apply: ab; apply/set_mem; apply: conva; rewrite !inE. by rewrite addrACA -!scalerDr. move=> t t1 ? /= [x Bx] <- B. have [->|t0] := eqVneq t 0. @@ -1761,7 +1693,7 @@ Definition seminorm_of := [set p : SemiNorm.type E | exists b, exists h : open_nbhsbasis_convextvs b, p = gauge_fun_basis h]. -#[local] Lemma seminorm_ofneq0 : seminorm_of !=set0. +Lemma seminorm_ofneq0 : seminorm_of !=set0. Proof. have [_ /(_ [set: E] filterT)] := basis_opennbhsbasis E; move=> [/= b Bb _]. exists (gauge_fun_basis Bb). @@ -1990,7 +1922,7 @@ move=> s0 /closed_Ndense; move=> /(_ s0). move=> /existsNP [U] /not_implyP [[x Ux]]. move=> /not_implyP [oU] /forallNP /= Uf. have [B Bconv [B0 Bbasis]] := (@locally_convex _ F). -have /nbhsE0 [V' /Bbasis [/= V BV VV'] VU]: nbhs x U by rewrite nbhsE; exists U. +have /nbhsE0 [_ [V' /Bbasis [/= V BV VV'] VU]]: nbhs x U by rewrite nbhsE; exists U. have [_ aV]: absolutely_convex_set V by apply: Bconv; rewrite inE. have nfU: forall z, V z -> f z != f x. move=> z Vz; apply/eqP => fzx.