wip subnormed

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -343,7 +343,7 @@ Import Lingraph.
 
  Variables (R : realType) (V : lmodType R) (F : pred V).
 
- Variables (F' : subLmodType F) (f : {linear F' -> R}) (p : V -> R).
+ Variables (F' : subLmodType F) (f : {linear F -> R}) (p : V -> R).
 
 
 (* MathComp seems to lack of an interface for submodules of V, so for now
@@ -378,35 +378,28 @@ End HahnBanach.
 
 
 (* To add once this is rebased over linear_continuous *)
-(* Section Substructures. *)
-(* Context (R: numFieldType) (V : normedModType R). *)
-(* Variable (A : pred V). *)
+Section Substructures.
+Context (R: numFieldType) (V : normedModType R).
+Variable (A : pred V).
 
-(* HB.instance Definition _ := NormedModule.on (subspace A). *)
+HB.instance Definition _ := NormedModule.on (subspace A).
 
-(* Check {linear_continuous (subspace A) -> R^o}. *)
+Check {linear_continuous (subspace A) -> R^o}.
 
-(* End Substructures. *)
+End Substructures.
 
 Section HBGeom.
 
 Variable (R : realType) (V : normedModType R) (F : pred V)
-(F' : subLmodType F) (f : {linear F' -> R}).
+ (f : {linear_continuous (subspace F) -> R}).
 
-(* once this is rebased over linear_continuous
-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].
+(* 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)) -> 
-(* hypothesis to delete once this is rebased over linear_continuous
-  and obtain through continuous_linear_bounded  *)
+(*   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.
-  move=> [r [ltr0 fxrx]].
+  have [r [ltr0 fxrx]] : exists2 r , (r > 0 ) & (forall z, `|f z| <=  `| z| * r). admit. 
   pose p:= fun x : V => `|x|*r.
  have convp: (@convex_function _ _ [set: V] p).
  rewrite /convex_function /conv => l v1 v2 _ _ /=.
@@ -419,7 +412,7 @@ Proof.
    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', f z <= p (\val z). 
+   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}.