diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1e22e3eaef..41ffdf50a6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,6 +21,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` @@ -43,6 +44,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` ### Changed @@ -83,6 +147,9 @@ + lemmas `closure_ballE`, `closed_ballxx`, `closed_ball_closed`, `subset_closed_ball`, `subset_closure_half`, `le_closed_ball` +- in `tvs.v`: + + mixin `Uniform_isConvexTvs` (now uses `absolutely_convex_set` and `nbhs_basis 0`) + ### Renamed - in `sequences.v`: @@ -96,6 +163,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` + ### Generalized - in `pseudometric_normed_Zmodule.v`: diff --git a/classical/classical_sets.v b/classical/classical_sets.v index a736a5caab..68917c321c 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., *) @@ -278,6 +281,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 *) @@ -1738,6 +1742,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 3b00d8cfc2..7e0645ae45 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -672,6 +672,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..5d64aabb18 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -18,7 +18,6 @@ From mathcomp Require Import reals convex topology normedtype. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -357,3 +356,93 @@ by exists g'. Qed. End hahn_banach_normed. + +Section hahn_banach_extension_ctvs. +Variable (R : realType) (V : convexTvsType R) (F : pred V). +(* In contrary to the normed case, the extension thm 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 *) +(* 7.1.2 Jarchow *) +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 /=. + apply: le_trans; first by exact : @ler_normD _ _ p (l%:num *: v1) (l%:num.~ *: v2). + rewrite !normZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//. + by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0. +have := (@hahn_banach_extension R V _ F' f p convp fp). +move=> [g majgp F_eqgf]. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + by apply/lcfun_seminorm; exists p; first by apply: 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. + + +(* A second version where F is a subspace of V, meaning endowed with the initial topology wrt to val*) +(* 7.2.1 Jarchow *) +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 /linear_continuous_seminorm: continuous (f : (init_subconvextvs F') -> R^o) by apply: continuous_fun. + move=> [p [cp ps] /= fp]. + have [/= nF] := cp. + move=> [] onF /= pF. + 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). + by exists bV; exists obV => //. + move=> z. + set pVz := (X in _ <= X). + apply: le_trans; first by apply: fp. + rewrite pF; apply: inf_le. + - move=> x /= [r [r0]]; rewrite inE => -[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 mulrC divff ?scale1r ?lt0r_neq0. + by rewrite scalerA divff ?scale1r ?lt0r_neq0. + - have [/= s s0 szbV]:= absorbing_opennbhsbasis obV (val z). + exists s^-1; split; rewrite ?invr_gt0 // inE /=; exists (s *: val z); first by apply/set_mem. + by rewrite scalerA mulrC divff ?scale1r ?lt0r_neq0. + - 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 by apply/set_mem. + by rewrite scalerA mulrC divff ?scale1r ?lt0r_neq0. +have convp : @convex_function _ _ [set: V] p'. (* or apply the previous thm but typing *) + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /=. + apply: le_trans; first by exact : @ler_normD _ _ p' (l%:num *: v1) (l%:num.~ *: v2). + rewrite !normZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//. + by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0. +have := (@hahn_banach_extension R V _ F' f p' convp fp'). +move=> [g majgp F_eqgf]. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + by apply/lcfun_seminorm; exists p'; first by apply: 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. + +Section hahn_banach_separation_ctvs. +(* TODO *) +End hahn_banach_separation_ctvs. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9cbedefad5..86ba2d322a 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 *) @@ -2034,10 +2042,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 3e64d90b49..1c0f743d94 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -163,7 +163,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) : @@ -171,9 +171,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. @@ -233,6 +245,21 @@ apply: cvg_pair; first exact: cvg_fst. by apply: continuous_comp; [exact: cvg_snd|exact: opp_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 1e91a170b7..b45da4a827 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")] @@ -93,10 +203,83 @@ HB.structure Definition TopologicalLmodule (K : numDomainType) := {M of TopologicalZmodule M & GRing.Lmodule K M & TopologicalZmodule_isTopologicalLmodule K M}. +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 (U : set E) (x : E) : open (+%R x @` U) -> open U. +Proof. +suff : U = ((+%R (-x) @` (+%R x @` U))). + by move => + H => ->; exact: openD. +apply/seteqP; split => z /=. + move=> Uz; exists (z + x); first by exists z => //; rewrite addrC. + by rewrite -addrCA [X in (_ + X = _)]addrC subrr addr0. +by move=> [y [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 nbhs0Z (R : numFieldType) (E : topologicalLmodType R) (U : set E) (r : R) : + r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ). +Proof. +move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. +rewrite scaler0 => /(_ U0)[]/= B [B1 B2] BU. +near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r. +by apply: (BU (r^-1, x)); split => //=; [exact: nbhs_singleton|near: x]. +Unshelve. all: by end_near. Qed. + +Lemma nbhsZ (R : numFieldType) (E : topologicalLmodType R) (U : set E) (r : R) + (x :E) : + r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ). +Proof. +move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U. +rewrite scalerA mulVf// scale1r =>/(_ U0)[] /= B [B1 B2] BU. +near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. +by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. +Unshelve. all: by end_near. Qed. + +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 {R : numFieldType} (E : topologicalType) (F : topologicalLmodType R). +Context {E : Type} {R : numFieldType} {F G : topologicalLmodType R}. -Lemma fun_cvgZ (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F) +Lemma cvgZ (U : set_system E) {FF : Filter U} (l : E -> R) (f : E -> F) (r : R) a : l @ U --> r -> f @ U --> a -> l x *: f x @[x --> U] --> r *: a. @@ -104,16 +287,71 @@ Proof. by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)). Qed. -Lemma fun_cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a : +Lemma cvgZr (U : set_system E) {FF : Filter U} k (f : E -> F) a : f @ U --> a -> k \*: f @ U --> k *: a. -Proof. by apply: fun_cvgZ => //; exact: cvg_cst. Qed. +Proof. by apply: cvgZ => //; exact: cvg_cst. 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 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. +#[deprecated(since="mathcomp-analysis 1.19.0", use=cvgZ)] +Notation fun_cvgZ := cvgZ (only parsing). +#[deprecated(since="mathcomp-analysis 1.19.0", use=cvgZr)] +Notation fun_cvgZr := cvgZr (only parsing). + +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. @@ -138,13 +376,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) := @@ -153,11 +402,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. + +HB.instance Definition _ := Uniform.on init_subconvextvs. +HB.instance Definition _ := GRing.Lmodule.on init_subconvextvs. -Let add_sub: continuous (fun x : sub_init_topo * sub_init_topo => x.1 + x.2). +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). @@ -166,28 +417,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). @@ -195,7 +443,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]. @@ -203,10 +451,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)))/=. @@ -218,9 +466,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)/=. @@ -230,83 +478,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. - -Lemma nbhsT_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_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. @@ -318,11 +528,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. @@ -335,7 +545,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)) : @@ -384,7 +594,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. @@ -397,9 +607,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). @@ -448,41 +660,281 @@ 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. -Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). -Proof. exact/nbhsT_subproof/add_continuous. Qed. +HB.builders Context R E & NbhsBasisAt0_isConvexTvs R E. -Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). -Proof. exact/nbhsB_subproof/add_continuous. Qed. +Let nbhs_fromfilter0 := @filter_from_basis0 R E (nbhsbasis_at0). -End ConvexTvs_numDomain. +#[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. -Section ConvexTvs_numField. +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. -Lemma nbhs0Z (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) : - r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ). +Let nbhs_singleton (p : E) (A : set E) : nbhs_fromfilter0 p A -> A p. Proof. -move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. -rewrite scaler0 => /(_ U0)[]/= B [B1 B2] BU. -near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r. -by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x]. -Unshelve. all: by end_near. Qed. +move=> [_/= [C f0C <-]]; apply; exists p => //; exists 0; rewrite ?addr0//. +exact: mem0_nbhsbasis_at0. +Qed. -Lemma nbhsZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) (x :E) : - r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ). +Let nbhs_nbhs (p : E) (A : set E) : nbhs_fromfilter0 p A -> + nbhs_fromfilter0 p (nbhs_fromfilter0^~ A). Proof. -move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U. -rewrite scalerA mulVf// scale1r =>/(_ U0)[] /= B [B1 B2] BU. -near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. -by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. -Unshelve. all: by end_near. Qed. +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. -End ConvexTvs_numField. +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. + +HB.builders Context R E & NbhsSubbasisAt0_isConvexTvs R E. + +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. + by move=> /= W; rewrite !inE => /orP[/fI/set_mem|/fJ/set_mem]. +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 standard_topology. Context {R : numFieldType}. @@ -493,8 +945,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//. @@ -502,14 +953,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 _ := @@ -536,28 +996,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 @@ -572,7 +1027,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) := { @@ -701,7 +1156,7 @@ HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f). #[local] Lemma lcfun_continuousM r g : continuous (r \*: g). -Proof. by move=> /= x; apply: fun_cvgZr; exact: continuous_fun. Qed. +Proof. by move=> /= x; apply: cvgZr; exact: continuous_fun. Qed. HB.instance Definition _ r g := isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g). @@ -734,3 +1189,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 fb373b9336..837a8cb083 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -127,6 +127,9 @@ Definition open_nbhs (p : T) (A : set T) := open A /\ A p. Definition basis (B : set_system T) := B `<=` open /\ forall x, 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 second_countable := exists2 B, countable B & basis B. Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p). @@ -514,6 +517,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 := { @@ -525,9 +535,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). @@ -577,8 +584,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 ;