Seminorm tvs

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`:

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.

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.

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.

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.

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.