update hahn_banach (wip)

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -939,18 +939,14 @@ Import numFieldNormedType.Exports.
 Local Open Scope classical_set_scope.
 
 Section HBGeom.
+Variable (R : realType) (V : normedModType R) (F : pred V) (f : V -> R) (F0 : F 0).
 
-Variable (R : realType) (V : normedModType R) (F : pred V) (f :  V -> R) (F0 : F 0).
-Hypothesis (linF : (forall (v1 v2 : V) (l : R),
-                       F v1 -> F v2 -> F (v1 + l *: v2))).
-Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 ->
-                              f (v1 + l *: v2) = f v1 + l * (f v2).
-
+Hypothesis linF : forall (v1 v2 : V) (l : R), F v1 -> F v2 -> F (v1 + l *: v2).
+Hypothesis linfF : forall v1 v2 l, F v1 -> F v2 -> f (v1 + l *: v2) = f v1 + l * (f v2).
 
 Hypothesis (Choice_prop : ((forall T U  (Q : T -> U -> Prop),
                       (forall t : T, exists u : U,  Q t u) -> (exists e, forall t,  Q t (e t))))).
 
-
 (*Looked a long time for within *)
 Definition continuousR_on ( G : set V ) (g : V -> R) :=
   {within G, continuous g}.
@@ -966,41 +962,43 @@ Lemma continuousR_scalar_on_bounded :
 Proof.
   rewrite /continuousR_on_at.
   move  => /cvg_ballP  H.
-    have H':  (0 < 1) by [].
-  move: (H 1) {H'}.
+  have H':  (0 < 1) by [].
+  have : \forall x \near within (fun x : V => F x) (nbhs 0), ball (f 0) 1 (f x).
+  apply: H. by [].
   have f0 : f 0 = 0.
      suff -> : f 0 = f (0 + (-1)*: 0) by rewrite linfF // mulNr mul1r addrN.
      by rewrite scaleNr scaler0 addrN.
-(*  rewrite near_simpl /( _ @ _ ) //= nearE /(within _ ) near_simpl f0.
+  rewrite /( _ @ _ ) //= nearE /(within _ ) f0 //=. rewrite near_simpl.
   rewrite -nbhs_nearE => H0 {H} ; move : (nbhs_ex H0) => [tp H] {H0}.
-  pose t := tp%:num .
-  exists (2*t^-1). split=> //.
+  (*pose t := tp%:num .  *)
+  exists (2*(tp%:num)^-1). split=> //.
   move=> x. case:  (boolp.EM (x=0)).
   - by move=> ->; rewrite f0 normr0 normr0 //= mul0r.
   - move/eqP=> xneq0 Fx.
-  pose a : V := (`|x|^-1 * t/2 ) *: x.
-  have Btp : ball 0 t a.
-   apply : ball_sym ; rewrite -ball_normE /ball_  subr0.
-   rewrite normmZ mulrC normrM.
-   rewrite !gtr0_norm //= ; last by rewrite  pmulr_lgt0 // invr_gt0 normr_gt0.
-   rewrite mulrC -mulrA -mulrA  ltr_pdivr_mull; last by rewrite normr_gt0.
-   rewrite mulrC -mulrA  gtr_pmull.
+  pose a : V := (`|x|^-1 * (tp%:num)/2 ) *: x.
+  have Btp : ball 0  (tp%:num) a.
+   apply : ball_sym ; rewrite -ball_normE /ball_ /=  subr0.
+   rewrite normrZ mulrC normrM.
+   rewrite !gtr0_norm //= ; last first.
+     rewrite  pmulr_lgt0 // ?invr_gt0 ?normr_gt0 //.
+   rewrite mulrC -mulrA -mulrA ltr_pdivrMl; last by rewrite normr_gt0.
+   rewrite mulrC -mulrA  gtr_pMl.
    rewrite invf_lt1 //=.
-     by have lt01 : 0 < 1 by []; have le11 : 1 <= 1 by [] ; apply : ltr_spaddr.
+     by rewrite ltr1n.
    by  rewrite pmulr_lgt0 // !normr_gt0.
  have Fa : F a by rewrite -[a]add0r; apply: linF.
  have :  `|f a| < 1.
     by move: (H _ Btp Fa); rewrite /ball /ball_ //= sub0r normrN.
-  suff ->  : ( f a =  ( (`|x|^-1) * t/2 ) * ( f x)) .
+  suff ->  : ( f a =  ( (`|x|^-1) * (tp%:num)/2 ) * ( f x)) .
      rewrite normrM (gtr0_norm) //.
-     rewrite mulrC mulrC  -mulrA  -mulrA  ltr_pdivr_mull //= ;
+     rewrite mulrC mulrC  -mulrA  -mulrA  ltr_pdivrMl //= ;
        last by rewrite normr_gt0.
-     rewrite mulrC [(_*1)]mulrC mul1r -ltr_pdivl_mulr //.
-     by rewrite invf_div => Ht; apply : ltW.
-     by  rewrite !mulr_gt0 // invr_gt0 normr_gt0.
- suff -> : a = 0+ (`|x|^-1 * t/2) *: x by rewrite linfF // f0 add0r.
+     rewrite mulrC [(_*1)]mulrC mul1r.
+     rewrite -[X in _ * X < _ ]invf_div ltr_pdivrMr //=; apply: ltW.
+     by rewrite !mulr_gt0  ?normr_gt0  // ?invr_gt0 normr_gt0.
+ suff -> : a = 0+ (`|x|^-1 * tp%:num /2) *: x by rewrite linfF // f0 add0r.
  by rewrite add0r.
-Qed.*) Admitted.
+Qed.
 
 Lemma mymysup : forall (A : set R) (a m : R),
      A a -> ubound A m ->
@@ -1028,17 +1026,15 @@ Lemma mymyinf : forall (A : set R) (a m : R),
   by move => x; apply: lb_le_inf.
 Qed.
 
-
 Notation myHB :=
   (HahnBanach (boolp.EM) Choice_prop mymysup mymyinf F0 linF linfF).
 
-
 Theorem HB_geom_normed :
-  continuousR_on_at F 0  f ->
+  continuousR_on_at F 0 f ->
   exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall x, F x -> (g x = f x)).
 Proof.
- move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}.
- pose p:= fun x : V => `|x|*r.
+  move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}.
+  pose p:= fun x : V => `|x|*r.
  have convp: hahn_banach_theorem.convex p.
    move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl.
    suff: `|l *: v1 + m *: v2|  <= (l * `|v1| + m * `|v2|).
@@ -1062,15 +1058,115 @@ Proof.
   apply: bounded_linear_continuous.
   exists r.
   split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *)
-(*
-  move => M m1; rewrite nbhs_ballP;  exists 1; first by [].
+  move => M m1; rewrite nbhs_ballP;  exists 1 => /=; first by [].
   move => y; rewrite -ball_normE //= sub0r => y1.
-  rewrite ler_norml; apply/andP; split.
-  - rewrite ler_oppl -linearN; apply: (le_trans (majgp (-y))).
-    by rewrite /p -[X in _ <= X]mul1r; apply: ler_pmul; rewrite ?normr_ge0 ?ltW //=.
+  rewrite ler_norml; apply/andP. split.
+  - rewrite lerNl  -linearN; apply: (le_trans (majgp (-y))).
+    by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
   - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN.
-    apply: ler_pmul; rewrite ?normr_ge0 ?ltW //=.
-Qed.*)
-Admitted.
+    apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+Qed.
+
 
 End HBGeom.
+
+
+Section newHBGeom.
+
+  (* TODO: port to ctvsType, by porting lemmas on continuous bounded linear functions there *)
+
+Variable (R : realType) (V: normedModType R) (F : subLmodType V) (f : {linear F -> R}).
+
+(* One needs to define the topological structure on F as the one induced by V, and make it  a normedModtype, as was done for subLmodType *)
+
+Hypothesis (Choice_prop : ((forall T U  (Q : T -> U -> Prop),
+                      (forall t : T, exists u : U,  Q t u) -> (exists e, forall t,  Q t (e t))))).
+
+(*
+Lemma mymysup : forall (A : set R) (a m : R),
+     A a -> ubound A m ->
+     {s : R | ubound A s /\ forall u, ubound A u -> s <= u}.
+Proof.
+  move => A a m Aa majAm.
+  have [A0 Aub]: has_sup A. split; first by exists a.
+    by exists m => x; apply majAm.
+  exists (reals.sup A).
+split.
+  by apply: sup_upper_bound.
+  by move => x; apply: sup_le_ub.
+Qed.
+
+(*TODO: should be lb_le_inf: *)
+Lemma mymyinf : forall (A : set R) (a m : R),
+     A a ->  lbound A m ->
+     {s : R | lbound A s /\ forall u, lbound A u -> u <= s}.
+  move => A a m Aa minAm.
+  have [A0 Alb]: has_inf A. split; first by exists a.
+    by exists m => x; apply minAm.
+  exists (reals.inf A).
+  split.
+    exact: ge_inf.
+  by move => x; apply: lb_le_inf.
+Qed.
+
+
+Notation myHB :=
+  (HahnBanach (boolp.EM) Choice_prop mymysup mymyinf F0 linF linfF).
+ *)
+
+ Search "continuous" "subspace".  
+(* bounded_linear_continuous: forall [R : numFieldType] [V W : normedModType R] [f : {linear V -> W}], bounded_near f (nbhs (0 : V)) -> continuous f
+linear_bounded_continuous: forall [R : numFieldType] [V W : normedModType R] (f : {linear V -> W}), bounded_near f (nbhs 0) <-> continuous f
+continuous_linear_bounded: forall [R : numFieldType] [V W : normedModType R] (x : V) [f : {linear V -> W}], {for 0, continuous f} -> bounded_near f (nbhs x) *)
+
+ (*TODO : clean the topological structure on F. Define subctvs ? *)
+Theorem new_HB_geom_normed :
+  continuous (f : (@initial_topology (sub_type F) V val) -> R) -> 
+  exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall (x : F), (g (val x) = f x)).
+Proof.
+  move /(_ 0) => /= H; rewrite /from_subspace /=.
+  have f0 : {for 0, continuous ( (f : (@initial_topology (sub_type F) V val) -> R))}.
+  admit.  
+  Check (continuous_linear_bounded).
+  (* TODO ; to apply this lemma, F needs to be given a normedmodtype structure *)
+ (*  move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}.
+  (* want :   r :
+  ltr0 : 0 < r
+  fxrx : forall x : V, F x -> `|f x| <= `|x| * r*)
+ pose p:= fun x : V => `|x|*r.
+ have convp: hahn_banach_theorem.convex p.
+   move=> v1 v2 l m [lt0l lt0m] addlm1 //= ; rewrite !/( p _) !mulrA -mulrDl.
+   suff: `|l *: v1 + m *: v2|  <= (l * `|v1| + m * `|v2|).
+     move => h; apply : ler_pM; last by [].
+     by apply : normr_ge0.
+     by apply : ltW.
+       by [].
+   have labs : `|l| = l by apply/normr_idP.
+   have mabs: `|m| = m by apply/normr_idP.
+   rewrite -[in(_*_)]labs -[in(m*_)]mabs.
+   rewrite -!normrZ.
+   by apply : ler_normD.
+ have majfp : forall x, F x -> f x <= p x.
+   move => x Fx; rewrite /(p _) ; apply : le_trans ; last by [].
+   apply : le_trans.
+   apply : ler_norm.
+   by apply : (fxrx x Fx).
+ move: (myHB convp majfp) => [ g  [majgp  F_eqgf] ] {majfp}.
+ exists g;  split; last by [].
+  move=> x; rewrite /cvgP; apply: (continuousfor0_continuous).
+  apply: bounded_linear_continuous.
+  exists r.
+  split; first by rewrite realE; apply/orP; left; apply: ltW. (* r is Numreal ... *)
+  move => M m1; rewrite nbhs_ballP;  exists 1 => /=; first by [].
+  move => y; rewrite -ball_normE //= sub0r => y1.
+  rewrite ler_norml; apply/andP. split.
+  - rewrite lerNl  -linearN; apply: (le_trans (majgp (-y))).
+    by rewrite /p -[X in _ <= X]mul1r; apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+  - apply: (le_trans (majgp (y))); rewrite /p -[X in _ <= X]mul1r -normrN.
+    apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
+Qed.
+*)
+Admitted.  
+
+
+End newHBGeom.

theories/tvs.v

@@ -861,7 +861,7 @@ Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _). Proof. by
 
 (* NB TODO: move section cvg_composition_pseudometric in normedtype.v here, to
 generalize it on tvstype *)
-(* Next lemmas are duplicates *)
+(* Next lemmas are duplicates  - do it more properly with appropriate conte*)
 (* TODO once PR1544 is merged *)
 
 Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :