clean

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -6,25 +6,12 @@ From mathcomp Require Import filter reals normedtype convex.
 Import numFieldNormedType.Exports.
 Local Open Scope classical_set_scope.
 
-(* Marie's proposal: encode the "partial" properties by reasoning on
-  the graph of functions. The other option would be to study a partial
-  order defined on subsets of the ambiant space V, on which it is possible
-  to obtain a bounded lineEar form extending f. But this options seems much
-  less convenient, in particular when establishing that one can extend f
-  on a space with one more dimension. Indeed, exhibiting a term of type
-  V -> R requires a case ternary analysis on F, the new line, and an
-  explicit direct sum to ensure the definition is exhaustive. Working with
-  graphs allows to leave this argument completely implicit. *)
-
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 
 
-
-
 Local Open Scope ring_scope.
 Local Open Scope convex_scope.
 Local Open Scope real_scope.
@@ -46,24 +33,24 @@ Variable f : graph.
 Hypothesis lrf : linear_graph f.
 
 Lemma lingraph_00 x r : f x r -> f 0 0.
- Proof.
- suff -> : f 0 0 = f (x + (-1) *: x) (r + (-1) * r) by move=> h; apply: lrf.
- by rewrite scaleNr mulNr mul1r scale1r !subrr.
- Qed.
+Proof.
+suff -> : f 0 0 = f (x + (-1) *: x) (r + (-1) * r) by move=> h; apply: lrf.
+by rewrite scaleNr mulNr mul1r scale1r !subrr.
+Qed.
 
- Lemma lingraph_scale x r l : f x r -> f (l *: x) (l * r).
- Proof.
- move=> fxr.
- have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r.
- by apply: lrf=> //; apply: lingraph_00 fxr.
- Qed.
+Lemma lingraph_scale x r l : f x r -> f (l *: x) (l * r).
+Proof.
+move=> fxr.
+have -> : f (l *: x) (l * r) = f (0 + l *: x) (0 + l * r) by rewrite !add0r.
+by apply: lrf=> //; exact: lingraph_00 fxr.
+Qed.
 
- Lemma lingraph_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2).
- Proof.
-     have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r.
-     have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r.
-     by apply: lrf.
- Qed.
+Lemma lingraph_add x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2)(r1 - r2).
+Proof.
+have -> : x1 - x2 = x1 + (-1) *: x2 by rewrite scaleNr scale1r.
+have -> : r1 - r2 = r1 + (-1) * r2 by rewrite mulNr mul1r.
+by exact: lrf.
+Qed.
 
 
  Definition add_line f w a := fun v r =>
@@ -73,6 +60,32 @@ Lemma lingraph_00 x r : f x r -> f 0 0.
 End Lingraphsec.
 End Lingraph.
 
+Section pos_quotient.
+Variable (R : realType).
+
+(* auxiliary lemmas that could be moved elsewhere *)
+
+Lemma divDl_ge0 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : 0 <= s / (s +t).
+by apply: divr_ge0 => //; apply: addr_ge0.
+Qed.
+ 
+Lemma divDl_le1 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :  s / (s +t) <= 1.
+move: s0; rewrite le0r => /orP []; first by move => /eqP ->; rewrite mul0r //.
+move: t0; rewrite le0r => /orP [].
+  by move => /eqP -> s0; rewrite addr0 divff //=; apply: lt0r_neq0. 
+by move=> t0 s0; rewrite ler_pdivrMr ?mul1r ?addr_gt0 // lerDl ltW.
+Qed.    
+
+Lemma divD_onem (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t).
+rewrite /(_).~.
+suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. 
+rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H.
+by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW.
+Qed.
+
+
+End pos_quotient.
+
 
 Section HBPreparation.
 Import Lingraph.
@@ -167,30 +180,13 @@ Definition zornS (z1 z2 : zorn_type):=
  Qed. 
 
 
- Variable g : zorn_type.
+Variable g : zorn_type.
 
- Hypothesis gP : forall z, zornS g z -> z = g.
+Hypothesis gP : forall z, zornS g z -> z = g.
 
- (*The next lemma proves that when z is of zorn_type, it can be extended on any
-  real line directed by an arbitrary vector v *)
+(*The next lemma proves that when z is of zorn_type, it can be extended on any
+real line directed by an arbitrary vector v *)
 
- Lemma divDl_ge0 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : 0 <= s / (s +t).
- by apply: divr_ge0 => //; apply: addr_ge0.
- Qed.
- 
- Lemma divDl_le1 (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) :  s / (s +t) <= 1.
- move: s0; rewrite le0r => /orP []; first by move => /eqP ->; rewrite mul0r //.
- move: t0; rewrite le0r => /orP [].
-   by move => /eqP -> s0; rewrite addr0 divff //=; apply: lt0r_neq0. 
- by move=> t0 s0; rewrite ler_pdivrMr ?mul1r ?addr_gt0 // lerDl ltW.
- Qed.    
-
- Lemma divD_onem (s t : R) (s0 : 0 < s) (t0 : 0 < t): (s / (s + t)).~ = t / (s + t).
- rewrite /(_).~.
- suff -> : 1 = (s + t)/(s + t) by rewrite -mulrBl -addrAC subrr add0r. 
- rewrite divff // /eqP addr_eq0; apply/negbT/eqP => H.
- by move: s0; rewrite H oppr_gt0 ltNge; move/negP; apply; rewrite ltW.
- Qed.
 
  Lemma domain_extend  (z : zorn_type) v :
      exists2 ze : zorn_type, (zornS z ze) & (exists r, (carrier ze)  v r).
@@ -201,12 +197,9 @@ Definition zornS (z1 z2 : zorn_type):=
  have c00 : c 0 0.
    have <- : phi 0 = 0 by rewrite linear0.
    by move: ps1; rewrite /extend_graph /= => /(_ 0) /=; rewrite GRing.val0; apply. 
- have [a aP] : exists a,  forall (x : V) (r lambda : R),
-       c x r -> r + lambda * a <= p (x + lambda *: v).
-   suff [a aP] : exists a,  forall (x : V) (r lambda : R),
-       c x r -> 0 < lambda ->
-       r + lambda * a <= p (x + lambda *: v) /\
-       r - lambda * a <= p (x - lambda *: v).
+ have [a aP] : exists a,  forall (x : V) (r lambda : R), c x r -> r + lambda * a <= p (x + lambda *: v).
+   suff [a aP] : exists a,  forall (x : V) (r lambda : R), c x r -> 0 < lambda ->
+       r + lambda * a <= p (x + lambda *: v) /\ r - lambda * a <= p (x - lambda *: v).
      exists a=> x r lambda cxr.
      have {aP} aP := aP _ _ _ cxr.
      case: (ltrgt0P lambda) ; [by case/aP | move=> ltl0 | move->]; last first.
@@ -216,8 +209,7 @@ Definition zornS (z1 z2 : zorn_type):=
      done.
    pose b (x : V) r lambda : R := (p (x + lambda *: v) - r) / lambda.
    pose a (x : V) r lambda : R := (r - p (x - lambda *: v)) / lambda.
-   have le_a_b x1 x2 r1 r2 s t : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t ->
-                                 a x1 r1 s <= b x2 r2 t.
+   have le_a_b x1 x2 r1 r2 s t : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t -> a x1 r1 s <= b x2 r2 t.
      move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b.
      rewrite ler_pdivlMr // mulrAC ler_pdivrMr // mulrC [_ * s]mulrC.
      rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr.
@@ -260,67 +252,58 @@ Definition zornS (z1 z2 : zorn_type):=
      pose alpha := ((sa + ib) / 2%:R).
      have le_alpha_ib : alpha <= ib by rewrite /alpha midf_le.
      have le_sa_alpha : sa <= alpha by rewrite /alpha midf_le.
-     exists alpha => x r l cxr lt0l; split.
+     exists alpha => x r l cxr lt0l; split. 
      - suff : alpha <= b x r l.
          by rewrite /b; move/ler_pdivlMr: lt0l->; rewrite lerBrDl mulrC.
        by apply: le_trans le_alpha_ib _; apply: ibdP; exists x; exists r; exists l.
      - suff : a x r l <= alpha.
-         rewrite /a. move/ler_pdivrMr: lt0l->.
-         by rewrite lerBlDl -lerBlDr mulrC.
-         by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l.
- pose z' := fun k r =>
-   exists v' : V, exists r' : R, exists lambda : R,
-         [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a].
- have z'_extends :  forall v r, c v r -> z' v r.
-   move=> x r cxr; exists x; exists r; exists 0; split=> //.
-   - by rewrite scale0r addr0.
-   - by rewrite mul0r addr0.
- have z'_prol : extend_graph z'.
-  move=> x; exists (val x); exists (phi x); exists 0; split=> //.
-   - by rewrite scale0r addr0.
-   - by rewrite mul0r addr0.
- - have z'_maj_by_p : le_graph p z'.
-   by move=> x r [w [s [l [cws -> ->]]]]; apply: aP.
- - have z'_lin : linear_graph z'.
+         by rewrite /a; move/ler_pdivrMr: lt0l-> ; rewrite lerBlDl -lerBlDr mulrC. 
+       by apply: le_trans le_sa_alpha; apply: ubdP; exists x; exists r; exists l.
+pose z' := fun k r =>  exists v' : V, exists r' : R, exists lambda : R,
+                        [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a].
+have z'_extends :  forall v r, c v r -> z' v r.
+  by move=> x r cxr; exists x; exists r; exists 0; split; rewrite // ?scale0r ?mul0r !addr0.
+have z'_prol : extend_graph z'.
+  by move=> x; exists (val x); exists (phi x); exists 0; split; rewrite // ?scale0r ?mul0r !addr0.
+have z'_maj_by_p : le_graph p z' by move=> x r [w [s [l [cws -> ->]]]]; apply: aP.
+have z'_lin : linear_graph z'.
    move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]].
    set w := (X in z' X _); set s := (X in z' _ X).
    have {w} -> : w = w1 + l *: w2 + (m1 + l * m2) *: v.
      by rewrite /w !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA.
    have {s} -> : s = s1 + l * s2 + (m1 + l * m2) * a.
      by rewrite /s !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA.
    exists (w1 + l *: w2); exists (s1 + l * s2); exists (m1 + l * m2); split=> //.
-   exact: ls1.
- - have z'_functional : functional_graph z'.
-   move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]].
-   have h1 (x : V) (r l : R) : x = l *: v ->  c x r -> x = 0 /\ l = 0.
-     move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r.
+   by exact: ls1.
+have z'_functional : functional_graph z'.
+  move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]].
+  have h1 (x : V) (r l : R) : x = l *: v ->  c x r -> x = 0 /\ l = 0.
+    move=> -> cxr; case: (l =P 0) => [-> | /eqP ln0]; first by rewrite scale0r.
      suff cvs: c v (l^-1 * r) by elim:nzv; exists (l^-1 * r).
      suff -> : v = l ^-1 *: (l *: v).
-       have -> :
-       c ( l ^-1 *: (l *: v)) (l^-1 * r) =  
-       c (0 + l ^-1 *: (l *: v)) (0 + l^-1 * r) by rewrite !add0r.
+       have -> : c(l^-1*:(l*:v))(l^-1*r) = c(0 + l^-1*:(l*:v))(0+l^-1*r) by rewrite !add0r.
        by apply: ls1=> //; apply: linrel_00 fxr.
      by rewrite scalerA mulVf ?scale1r.
    have [rw12 erw12] : exists r,  c (w1 - w2) r.
-     exists (s1 + (-1) * s2).
+     exists (s1+(-1)*s2).
      have -> : w1 - w2 = w1 + (-1) *: w2 by rewrite scaleNr scale1r.
      by apply: ls1.
    have [ew12 /eqP]: w1 - w2 = 0 /\ (m2 - m1 = 0).
      apply: h1 erw12; rewrite scalerBl; apply/eqP; rewrite subr_eq addrC addrA.
      by rewrite -subr_eq opprK e1.
    suff -> : s1 = s2 by rewrite subr_eq0=> /eqP->.
    by apply: fs1 cws2; move/eqP: ew12; rewrite subr_eq0=> /eqP<-.
- have z'_spec : le_extend_graph z' by split.
- pose zz' := ZornType z'_spec.
- exists zz'; rewrite /zornS => //=; exists a; exists 0; exists 0; exists 1.
- by rewrite add0r mul1r scale1r add0r; split.
- Qed.
+have z'_spec : le_extend_graph z' by split.
+pose zz' := ZornType z'_spec.
+exists zz'; rewrite /zornS => //=; exists a; exists 0; exists 0; exists 1.
+by rewrite add0r mul1r scale1r add0r; split.
+Qed.
 
- Let tot_g v : exists r, carrier g v r.
- Proof.
- have [z /gP sgz [r zr]]:= domain_extend g v.
- by exists r; rewrite -sgz.
- Qed.
+Let tot_g v : exists r, carrier g v r.
+Proof.
+have [z /gP sgz [r zr]]:= domain_extend g v.
+by exists r; rewrite -sgz.
+Qed.
 
 
 Lemma hb_witness : exists h : V -> R, forall v r, carrier g v r <-> (h v = r).
@@ -331,7 +314,7 @@ by have -> // := fg v r (h v).
 Qed.
 
 
- End HBPreparation.
+End HBPreparation.
 
 
 Section HahnBanach.
@@ -436,7 +419,6 @@ have contg: (continuous (g : V -> R)).
     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 //=.
-    (* 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'.