wip linear continuous

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -340,16 +340,14 @@ Import Lingraph.
 (* We consider R a real (=ordered) field with supremum, and V a (left) module
    on R. We do not make use of the 'vector' interface as the latter enforces
    finite dimension. *)
-  
- Variables (R : realType) (V : lmodType R) (F : pred V).
 
- Variables (F' : subLmodType F) (f : {linear F -> R}) (p : V -> R).
+(* DO NOT USE subLmodtype but the following *)
+  
+Variables (R : realType) (V : lmodType R) (F : pred V).
 
+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
-   we state "by hand" that F is closed under linear combinations. *)
-
-Hypothesis p_cvx : (@convex_function  R V [set: V]  p).
+Hypothesis p_cvx : (@convex_function R V [set: V] p).
 
 Hypothesis f_bounded_by_p : forall (z : F'), (f z  <= p (\val z)).
 
@@ -376,31 +374,100 @@ Qed.
 
 End HahnBanach.
 
-
-(* To add once this is rebased over linear_continuous *)
 Section Substructures.
 Context (R: numFieldType) (V : normedModType R).
-Variable (A : pred V).
+Variable (A : pred V) (A': subLmodType A).
 
 HB.instance Definition _ := NormedModule.on (subspace A).
 
 Check {linear_continuous (subspace A) -> R^o}.
+(* NB : I'm afraid this describes a function continuous on A but linear on the whole V *)
+
+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
+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)) -> 
+(* hypothesis to delete once this is rebased over linear_continuous
+  and obtain through continuous_linear_bounded  *)
+  exists g: {linear_continuous V -> R}, (forall x, (g (val x) = f x)).
+Proof.
+  move=> [r [ltr0 fxrx]].
+  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', 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=> 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 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]. *)
+(*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). admit. 
-  pose p:= fun x : V => `|x|*r.
+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.
@@ -412,7 +479,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 z <= p ( 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}.
@@ -430,4 +497,5 @@ Proof.
     apply: ler_pM; rewrite ?normr_ge0 ?ltW //=.
 Qed.     
 
-End HBGeom.
+End newHBGeom.
+*)

theories/normedtype_theory/tvs.v

@@ -703,7 +703,7 @@ Context {R : numDomainType} {E F : NbhsLmodule.type R}
 Let lcfun_comp_subproof1 : linear_for s (g \o f).
 Proof. by move=> *; move=> *; rewrite !linearP. Qed.
 
-Let lcfun_comp_subproof2 : continuous (g \o f).
+Let lcfun_comp_subproof2 : continuous (g \o f). 
 Proof. by move=> x; apply: continuous_comp; exact/cts_fun. Qed.
 
 HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
@@ -731,7 +731,7 @@ HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
 Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
   f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
 Proof.
-move=> fa ga.
+move=> fa ga. 
 by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..].
 Qed.
 
@@ -782,3 +782,16 @@ HB.instance Definition _ :=
   [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
 
 End lcfun_lmodtype.
+
+
+Section lcfunproperties.
+Context {R : numDomainType} {E F : NbhsLmodule.type R}
+  (f : {linear_continuous E -> F}).
+
+Lemma lcfun_continuous : continuous f. 
+Proof. exact: cts_fun. Qed.
+
+Lemma lcfun_linear : linear f. 
+Proof. move => *; exact: linearP. Qed.
+
+End lcfunproperties.