wip linear_continuous

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -387,13 +387,13 @@ Check ((subspace A : normedModType R)).
 
 End Substructures.
 
-(*
+
 Section HBGeom.
 
 Variable (R : realType) (V : normedModType R) (F : pred V)
 (F' : subLmodType F) (f : {linear F' -> R}).
 
-(* once this is rebased over linear_continuous
+(* once subnormedspaces are correctly defined replace by
 Variable (R : realType) (V : normedModType R) (F : pred V)
 (f : {linear_continuous (subspace F) -> R}).
 *)
@@ -423,79 +423,21 @@ Proof.
    have majfp : forall z : F', f z <= p (\val z). 
    move => z; rewrite /(p _) ; apply : le_trans; last by []. 
    by apply : ler_norm.
- move: (HahnBanach convp majfp) => [ g  [majgp  F_eqgf] ] {majfp}.
- have cg: continuous g. admit.
- have lg: linear g by  move => *; apply: linearP.
- pose glin := GRing.isLinear.Build _ _ _ _ g lg.
- Search  "Continuous" "Build". 
- pose (g' : {linear_continuous V -> R}) := HB.pack g glin
- exists g ;  split; last by [].
+   move: (HahnBanach convp majfp) => [g] [majgp  F_eqgf] {majfp}.
+have ling :(linear (g : V -> R)) by exact:linearP.   
+have contg: (continuous (g : V -> R)).  
   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 ... *)
+  exists r; split; first by exact: gtr0_real. 
   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.     
-
-End HBGeom.
-
-
-Section newHBGeom.
-
-Variable (R : realType) (V : normedModType R) (F : pred V)
- (f : {linear_continuous (subspace F) -> R}).
-
-(*Let setF := [set x : V  | exists (z : F'), val z = x].*)
-
-Theorem HB_geom_normed :
-(*   exists  r , (r > 0 ) /\ (forall (z : F'), (`|f z| ) <=  `|(val z)| * r)) ->  *)
-  exists g: {linear_continuous V -> R}, (forall x : V, F x -> (g x = f x)).
-Proof.
-have [r [ltr0 fxrx]] : exists2 r , (r > 0 ) & (forall z, `|f z| <=  `| z| * r).
-  have :  bounded_near f (nbhs 0). 
-  Check (@continuous_linear_bounded _ _ _ 0 f).
-  have H: { for 0, continuous f} by apply: cts_fun.
-  Fail Check (@continuous_linear_bounded _ _ _ 0 f H).
-  have H': { for (0 : subspace F), continuous f} by apply: cts_fun.
-  Fail Check (@continuous_linear_bounded _ _ _ 0 f H').
-  admit.
-  Fail apply/linear_boundedP.
- (* Lemmas for normedspaces do not seem to work on subspace F *) 
- pose p:= fun x : V => `|x|*r.
- have convp: (@convex_function _ _ [set: V] p).
- rewrite /convex_function /conv => l v1 v2 _ _ /=.
- rewrite [X in (_ <= X)]/conv /= /p.
- apply: le_trans.
-   have H  :  `|l%:num *: v1 + (l%:num).~ *: v2|  <=  `|l%:num *: v1|  + `|(l%:num).~ *: v2|.
-     by apply: ler_normD.
-   by apply: (@ler_pM _ _ _ r r _ _ H) => //; apply: ltW.
-   rewrite mulrDl !normrZ -![_ *: _]/(_ * _).
-   have -> : `|l%:num| = l%:num by apply/normr_idP.
-   have -> : `|(l%:num).~| = (l%:num).~ by apply/normr_idP; apply: onem_ge0.
-   by rewrite !mulrA. 
- have majfp : forall z, f z <= p ( z). 
-   move => z; rewrite /(p _) ; apply : le_trans; last by []. 
-   by apply : ler_norm.
- move: (HahnBanach 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.     
-
-End newHBGeom.
-*)
+    (* TODO  : build g with HB.build and HB.pack *)
+pose Hg := isLinearContinuous.Build _ _ _ _ g ling contg.     
+pose g': {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) Hg.
+by exists g'.
+Qed.