Hausdorff ctvs

CHANGELOG_UNRELEASED.md

@@ -3,6 +3,29 @@
 ## [Unreleased]
 
 ### Added
+- in `topology_structure.v`
+  + lemma `closed_Ndense`
+
+- in `pseudometric_normed_Zmodule.v`
+  + lemma `nbhs0_add`
+  + lemma `hausdorff_convextvs`
+
+- in `tvs.v`
+  + lemma `closure_convextvs`, `closure_addset`
+  + lemma `accessible field`
+  + lemma `hausdorff_init_convextvs`
+  + definition `closed_nbhsbasis_convextvs`
+  + lemma `has_closed_nbhs_basis`
+  + lemma `hausdorff_seminorm_on`
+  + lemma `seminorm_of_neq0`
+  + lemma `continuous_closedkernel`
+
+- in `hahn_banach_theorem.v`
+  + definition `linepred` and `line`
+  + lemma `line_linepred`
+  + subLmodule structure on `line`
+  + lemma `scaler_eq0` and `sclaeIl` (TO BE MOVED)
+  + lemma hahn_banach_extension_hausdorff
 
 - in `exp.v`:
   + lemmas `cvgy_expR`, `cvgNy_expR`, `lny`, `ge0_lt1_powR_cvg0`, 
@@ -41,4 +64,4 @@
 
 ### Infrastructure
 
-### Misc
+### Misc

theories/functional_analysis/hahn_banach_theorem.v

@@ -27,6 +27,10 @@ From mathcomp Require Import reals convex topology normedtype.
 (* | hahn_banach_extension_normed         | subNormedmodType | normedModType |*)
 (* | hahn_banach_extension_subcvts        | subconvextvsType | convexTvsType |*)
 (* | hahn_banach_extension_initialsubctvs | subLmodType      | convexTvsType |*)
+(*                                                                            *)
+(* Theorem `hahn_banach_extension_hausdorff` states, given a non-null point   *)
+(* in a convexTvsType, the existence of a linear continuous form non-null at  *)
+(* this point.                                                                *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -367,6 +371,38 @@ Qed.
 
 End hahn_banach_normed.
 
+
+
+Section line_lmodtype.
+(**md this section construct the subLmodType structure on a line generated by an
+element of a lmodType. It is necessary to prove hahn_banach_separation_hausdorff
+below *)
+Variable (R : numDomainType) (V: lmodType R) (x : V).
+
+Definition linepred  : {pred V} :=   mem [set y | exists t, y = t *: x ].
+Definition line := {y | linepred y}.
+
+Lemma line_linepred (y : line) : exists t, val(y) == t *: x.
+Proof.
+by move: y => [yv] /= /asboolP [t] ->; exists t.
+Qed.
+
+#[local] Lemma line_submod_closed : submod_closed (linepred).
+Proof.
+split; first by rewrite inE; exists 0; rewrite scale0r.
+move=> t y z; rewrite !inE => -[ty ->] -[tz ->]; exists (t * ty + tz).
+by rewrite scalerDl scalerA.
+Qed.
+
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _  linepred line_submod_closed.
+
+HB.instance Definition _ := SubChoice.on line.
+
+HB.instance Definition _ := [SubChoice_isSubLmodule of line  by <:].
+
+End line_lmodtype.
+
 Section hahn_banach_extension_ctvs.
 Context {R : realType} {V : convexTvsType R} (F : pred V).
 (**md Contrary to the normed case, the extension theorem is not true for any
@@ -457,3 +493,82 @@ by exists g'.
 Qed.
 
 End hahn_banach_extension_ctvs.
+
+(* TBA : to classical ? Where shoudl this go *)
+Lemma scaler_eq0 (R : numFieldType) (V: lmodType R) (a : V) t :
+  a != 0 -> (t *: a = 0 -> t = 0).
+Proof.
+move=> a0 ta; apply: contrapT => /eqP t0.
+have : t^-1 *: (t *: a) = 0 by rewrite ta scaler0.
+by rewrite scalerA mulVf// scale1r; apply/eqP.
+Qed.
+
+Lemma scaleIl (R : numFieldType) (V: lmodType R) (a : V) :
+  a != 0 -> injective (fun t => t *: a).
+Proof.
+move=> a0 s t => /eqP; rewrite -subr_eq0 -scalerBl=> /eqP /(scaler_eq0 a0) /eqP.
+by rewrite subr_eq0 => /eqP.
+Qed.
+(*END TBA *)
+
+(* 7.2.3 in Jarchow *)
+Corollary hahn_banach_extension_hausdorff (R : realType) (V : convexTvsType R) :
+  hausdorff_space V <->
+  forall x : V,  x != 0 -> exists l : {linear_continuous V -> R^o}, l x != 0.
+Proof.
+split; last first.
+(* proof in here is different than in the book - Jarchow mentions "a" continuous
+seminorm in 7.2.3 but refers to 2.7.1 which proves the results for a seminorm of
+the set of seminorms generating the topology - it probably lacks an argument
+saying that continuous seminorms are always bounded by this set of seminorms,
+which we haven't formalised here *)
+  move => H.
+  pose P := @seminorm_of R V.
+  pose P0 := @seminorm_ofneq0 R V.
+  suff : hausdorff_space (seminorm_on P0).
+    have [contVs _ ] := @seminorm_convextvs _ V.
+    by move=> + x y cs; apply => a b /contVs nsa /contVs nsb; exact: cs.
+  apply/hausdorff_seminorm_on=> x /H [l].
+  have [l0|l0|] := ltrgtP (l x) (0 : R) => //.
+    have /linear_continuous_seminorm[p [sp _]/= lp] :=
+  @continuous_fun _ _ (-1 *: l).
+    exists p => //; apply: lt_le_trans (lp _).
+    by rewrite scaleN1r ltrNr oppr0.
+  have /linear_continuous_seminorm[p [sp _] /= lp] := @continuous_fun _ _ l.
+  by exists p => //; exact: lt_le_trans (lp _).
+move=> haus x x0.
+pose l := fun y : line x => xchoose (line_linepred y).
+have llinear : linear_for ( *:%R) l.
+  rewrite /l /= => t /= u v; apply: scaleIl; first exact: x0.
+  rewrite scalerDl -scalerA.
+  move/eqP : (xchooseP (line_linepred u)) => <-.
+  move/eqP : (xchooseP (line_linepred v)) => <-.
+  move/eqP : (xchooseP (line_linepred (t *: u + v))) => <-.
+  by rewrite (@GRing.valD _ _ (line x)) GRing.valZ.
+pose linlP := GRing.isLinear.Build _ _ _ _ l llinear.
+pose linl : {linear (init_subconvextvs (line x)) -> R^o} := HB.pack l linlP.
+have lcont : continuous linl.
+  apply/continuous_closedkernel.
+  have -> : linl @^-1` [set 0] = [set 0].
+    apply/seteqP; split => u /=.
+      move/eqP : (xchooseP (line_linepred u)) => /[swap]; rewrite /l => ->.
+      by rewrite scale0r -(@GRing.val0 _ _ (line x)) => /val_inj.
+    move=> u0; move/eqP: (xchooseP (line_linepred u)).
+    rewrite u0 /= /l; move/eqP; rewrite eq_sym => /eqP.
+    by move/(scaler_eq0 x0).
+  apply: accessible_closed_set1; apply: hausdorff_accessible.
+  exact: hausdorff_init_convextvs.
+pose contlP := isContinuous.Build _ _ _ lcont.
+pose lcl : {linear_continuous (init_subconvextvs (line x)) -> R^o} :=
+  HB.pack (l : (init_subconvextvs (line x)) -> R^o) linlP contlP.
+have := (hahn_banach_extension_initialsubctvs lcl) => -[g Pg]; exists g.
+have xlinepred : (linepred x) x by apply/asboolP; exists 1; rewrite scale1r.
+pose xline := exist (linepred x) _ xlinepred; have <- : \val xline = x by [].
+rewrite Pg.
+suff -> : lcl xline = 1 by [].
+move/eqP : (xchooseP (line_linepred xline)).
+have {1}-> : \val xline = x by []; rewrite -{1}(scale1r (x : V)).
+by move/scaleIl => /(_ _)/esym; exact.
+Qed.
+
+(* TODO : more hahn banach separation theorems *)

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -6,7 +6,7 @@ From mathcomp Require Import interval interval_inference archimedean.
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import set_interval ereal reals topology.
-From mathcomp Require Import num_normedtype.
+From mathcomp Require Import num_normedtype contra.
 
 (**md**************************************************************************)
 (* # Normed topological abelian groups                                        *)
@@ -261,6 +261,32 @@ apply: funext => z /=; apply: propext; split=> [Az|[_ -> [y By]]].
 by rewrite addrC => /addIr <-.
 Qed.
 
+Lemma nbhs0_add (A : set M) : nbhs 0 A ->  exists2 B, nbhs 0 B & B `+ B `<=` A.
+Proof.
+move=> na.
+have := add_continuous 0 A.
+rewrite add0r => /(_ na) /= -[[b1 b2] /= [n1 n2] ba].
+exists (b1 `&` b2); first exact: filterI.
+by move => z /= [x [x1 _]] [y [_ y2]] <-; exact: (ba (x, y)).
+Qed.
+
+Lemma hausdorff_convextvs : hausdorff_space M <-> closed [set 0 : M].
+Proof.
+split=> [|cl].
+  move=> /(_ (0:M)) hF x /= cl; apply/esym/hF.
+  move=> a b n0a /(cl b) [? [-> b0]].
+  by exists 0; split => //; exact: nbhs_singleton.
+(* NB: simpler proof using the closed subbasis? *)
+move=> x y H; apply: subr0_eq.
+move: (H); contra => xy0.
+have nxy : nbhs (x - y) (~` [set 0]).
+  by apply: open_nbhs_nbhs; split => /=; [exact: closed_openC|exact/eqP].
+have /(_ (~` [set 0]) nxy) [] : continuous_at (x, y) (fun z => z.1 - z.2).
+  exact: sub_continuous.
+move=> [a b] /= [na nb] ab0; exists a; exists b => //; split => // z az bz.
+by have := ab0 (z, z) => /=; rewrite subrr; exact.
+Qed.
+
 End TopologicalZmoduleTheory.
 
 HB.factory Record PreTopologicalNmodule_isTopologicalZmodule M