update hahn_banach, get rid of admit

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -974,37 +974,35 @@ Proof.
      by rewrite scaleNr scaler0 addrN.
   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=> //.
-    admit. 
+  (*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.
+  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 //. admit. 
+     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 rewrite ltr1n. 
-     (*by have lt01 : 0 < 1 by []; have le11 : 1 <= 1 by [] ; apply : ltr_pDl.
    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 ->
@@ -1040,7 +1038,8 @@ Theorem HB_geom_normed :
   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|).
@@ -1125,16 +1124,17 @@ Notation myHB :=
 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 :
-  {within [set` F],  continuous f} -> 
-  exists g: {scalar V}, (continuous (g : V -> R)) /\ (forall x, F x -> (g x = f x)).
+  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.
-  (*
-  Search "continuous" "linear" "bounded".
   move /(_ 0) => /= H; rewrite /from_subspace /=.
-  have f0 : {for 0, continuous f}. admit (*F needs to be open ?*).
-  Check ( continuous_linear_bounded). _ f0).
-  move=> H; move: (continuousR_scalar_on_bounded H) => [r [ltr0 fxrx]] {H}.
+  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*)
@@ -1171,7 +1171,7 @@ Proof.
     apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
 Qed.
 *)
-
+Admitted. 
 
 
 End HBGeom.