convexW

Author: affeldt-aist

theories/tvs.v

@@ -346,7 +346,19 @@ Local Open Scope convex_scope.
 Definition convex (R : numDomainType) (M : lmodType R)
     (A : set (convex_lmodType M))(* try to get rid of the convex_lmodType *) :=
   forall x y lambda, x \in A -> y \in A -> x <| lambda |> y \in A.
-(*  0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A *)
+
+Lemma convexW (R : numDomainType) (M : lmodType R) (A : set (convex_lmodType M)) :
+  convex A <->
+  {in A &, forall x y (k : {i01 R}), 0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}.
+Proof.
+split => [cA x y xA yA k k0 k1|cA x y l xA yA].
+  by have /(_ k) := cA _ _ _ xA yA.
+have [->|l0] := eqVneq l 0%:i01; first by rewrite conv0.
+have [->|l1] := eqVneq l 1%:i01; first by rewrite conv1.
+apply: cA => //.
+- by rewrite lt_neqAle eq_sym l0 ge0.
+- by rewrite lt_neqAle l1 le1.
+Qed.
 
 (*TODO : name it convexTvs*)
 HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E
@@ -591,49 +603,29 @@ rewrite -mulrBl normrM (@le_lt_trans _ _ (`|k - z1| * M)) ?ler_wpM2l//.
 by rewrite -ltr_pdivlMr ?(lt_le_trans k1r) ?normr_gt0.
 Qed.
 
-Lemma le0i (l : {i01 R}) : (l <= 0%:i01) = (l == 0%:i01).
-Proof.
-apply/idP/idP.
-  rewrite eq_le => ->/=.
-  apply: ge0 => //=.
-  admit. (* ask Pierre *)
-by rewrite eq_le => /andP[].
-Admitted.
-
-Lemma le1i (l : {i01 R}) : (1%:i01 <= l) = (l == 1%:i01).
-Proof.
-apply/idP/idP.
-  rewrite eq_le => ->/=.
-  rewrite andbT.
-  apply: le1 => //=.
-  admit. (* ask Pierre *)
-by rewrite eq_le => /andP[].
-Admitted.
-
 Local Lemma standard_locally_convex :
   exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B.
 Proof.
 (* NB(rei): almost the same code as in normedtype.v *)
 exists [set B | exists x r, B = ball x r].
-  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
-  rewrite !inE /ball /= => zx yx.
-  have [l0|] := ltP 0%:i01 l; last by rewrite le0i => /eqP ->; rewrite conv0.
-  have [l1|] := ltP l 1%:i01; last by rewrite le1i => /eqP ->; rewrite conv1.
+  move=> b/= /[!inE]/= [[x]] [r] ->.
+  apply/convexW => z y; rewrite /ball/= !inE/= => zx yx l /[!inE]/= l0 l1.
+  (* conv lemma? *)
   have -> : x = x <| l |> x by rewrite convmm. (*TODO: this looks superfluous *)
-  rewrite [X in `|X|](_ : _ =
-      l%:num *: (x - z) + (l%:num.~) *: (x - y)); last first.
+  rewrite [X in `|X|](_ : _ = (x - z) <| l |> (x - y)); last first.
     by rewrite opprD addrACA -mulrBr -mulrBr.
-  rewrite (@le_lt_trans _ _ (l%:num * `|x - z| + l%:num.~ * `|x - y|))//.
+  rewrite (@le_lt_trans _ _ ((`|x - z| : R^o) <| l |> `|x - y|))//.
     rewrite -[in X in _ <= X + _](@ger0_norm _ l%:num)//.
     rewrite -[in X in _ <= _ + X](@ger0_norm _ l%:num.~) ?subr_ge0//.
-    rewrite -!normrM -mulr_algl.
-    rewrite /GRing.scale/= mulr1.
+    rewrite [X in `|X| <= _](_ : _ = l%:num * (x - z) + l%:num.~ * (x - y))//.
+    rewrite -[X in _ <= X + _]normrM.
+    rewrite -[X in _ <= _ + X]normrM.
     by rewrite ler_normD.
-  rewrite (@lt_le_trans _ _ (l%:num * r + l%:num.~ * r ))//.
+  rewrite (@lt_le_trans _ _ ((r : R^o) <| l |> r))//.
     rewrite ltr_leD//.
       by rewrite ltr_pM2l// normr_gt0// gt_eqF.
     by rewrite ler_wpM2l// ?subr_ge0// ltW.
-  by rewrite -mulrDl subrKC mul1r.
+  by rewrite convmm.
 split.
   move=> B [x] [r] ->.
   rewrite openE/= /ball/= /interior => y /= bxy; rewrite -nbhs_ballE.