Seminorm tvs

CHANGELOG_UNRELEASED.md

@@ -234,6 +234,61 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in `unstable.v`:
+  + lemma `seminorm_normrB`
+
+- in `initial_topology.v`:
+  + lemma `initial_nbhs_preimage`
+
+- in `topology_structure.v`:
+  + definition `nbhs_basis`
+  + definition `open_from`
+
+- in `normed_module.v`:
+  + lemma `ball_convex_set` (was a `Let`)
+
+- in `tvs.v`:
+  + definition `balanced_set`
+  + definition `absolutely_convex_set`
+  + lemma `absolutely_convex0`
+  + definition `absorbing_set`
+  + lemma `absolutely_convex_setX`
+  + notation `... `+ ...`
+  + lemmas `addsetS`, `add0set`, `addsetI`, `addsetA`
+  + lemma `continuous_shift`
+  + lemma `nbhs_add1set`
+  + 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`
+
 ### Changed
 
 - in `realsum.v`:
@@ -354,6 +409,9 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- from `normed_module.v` to `tvs.v`:
+  + lemma `continuousfor0_continuous` (moved and generalized)
+
 ### Renamed
 
 - in `tvs.v`:
@@ -407,6 +465,13 @@
 - in `functions.v`
   + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`)
 
+- in `tvs.v`:
+  + lemma `nbhsT_subproof` -> `nbhsD_subproof`
+
+- in `tvs.v`:
+  + lemma `nbhsT` -> `nbhsD0`
+  + lemma `nbhsB` -> `nbhsD`
+
 ### Generalized
 
 - in `measurable_structure.v`:

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/functional_analysis/hahn_banach_theorem.v

@@ -358,3 +358,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 extention 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

@@ -132,7 +132,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/=.
@@ -145,16 +145,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.
 
 HB.instance Definition _ :=
@@ -2012,10 +2020,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.