From a3de8e54fa2f255bdf579eb9c78eb9533f6ebcee Mon Sep 17 00:00:00 2001
From: mkerjean <kerjean@lipn.fr>
Date: Fri, 13 Sep 2024 22:31:18 +0200
Subject: [PATCH] convex

---
 theories/normedtype.v | 37 +++++++++++++++----------------------
 theories/tvs.v        |  2 +-
 2 files changed, 16 insertions(+), 23 deletions(-)

diff --git a/theories/normedtype.v b/theories/normedtype.v
index d8852505fe..d1d7059b27 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -852,30 +852,22 @@ Qed.
 Lemma locally_convex : exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B.
 Proof.
 exists [set B | exists x, exists r, B = ball x r].
-  move=> b; rewrite inE /= => [[x]] [r] -> z y l. 
-  rewrite !inE -!ball_normE /= => zx yx l1.
-  (* have xz : `|z| < r + `|x|.  *)
-  (*   have -> : `|z| = `|(z - x) + x| by rewrite -addrA [X in (_+X)]addrC subrr addr0.   *)
-  (*   rewrite (@lt_le_trans _ _ (r + normr x )) //. *)
-  (*   rewrite (@le_lt_trans _ _ (normr ((x - z)%R) + normr x)) //. *)
-  (*   rewrite -[in X in (_ <= X)]opprB normrN ler_normD // addrC. *)
-  (*   by rewrite (@ltr_leD _ _ _ (normr x) _ zx) //. *)
-  (* have xy : `|y| < r + `|x|.   *)
-  (*   have -> : `|y| = `|(y - x) + x| by rewrite -addrA [X in (_+X)]addrC subrr addr0. *)
-  (*   rewrite (@lt_le_trans _ _ (r + normr x )) //. *)
-  (*   rewrite (@le_lt_trans _ _ (normr ((y - x)%R) + normr x)) //.  *)
-  (*     by rewrite ler_normD // addrC. *)
-  (*   by rewrite (@ltr_leD _ _ _ (normr x) _ yx) //=. *)
-  have ->:  x = l *: x + (1-l) *: x. admit.
-  have -> :
+  move=> b; rewrite inE /= => [[x]] [r] -> z y l.
+  rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1.
+  have ->:  x = l *: x + (1-l) *: x by rewrite scalerBl addrCA subrr addr0 scale1r.
+    have -> :
   (l *: x + (1 - l) *: x) - (l *: z + (1 - l) *: y) = (l *: (x-z) + (1 - l) *: (x - y)).
-  rewrite opprD. rewrite addrCA.  admit.
+  by rewrite opprD addrCA addrA addrA -!scalerN -scalerDr [X in l*:X]addrC -addrA -scalerDr.
   rewrite (@le_lt_trans _ _ ( `|l| * `|x - z| + `|1 - l| * `|x - y|)) //.
     by rewrite -!normrZ ?ler_normD //.
-    rewrite (@lt_trans _ _ ( `|l| * r + `|1 - l| * r )) //.
-    rewrite ltrD //. rewrite le_lt_pM  //. normrN. 
-  have -> : normr (1 -l) = 1 - normr l. admit.  
-  rewrite -mulrDl addrCA subrr addr0.
+    rewrite (@lt_le_trans _ _ ( `|l| * r + `|1 - l| * r )) //.
+    rewrite ltr_leD //.
+    rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?lt0r_neq0 //.
+    rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE;
+    by apply/eqP =>  H; move: l1; rewrite H // lt_def => /andP [] /eqP //=.
+  have -> : normr (1 -l) = 1 - normr l.
+    by move/ltW/normr_idP: l0 => ->; move/ltW/normr_idP: l1 => ->.
+  by rewrite -mulrDl addrCA subrr addr0 mul1r.
 split =>  /=.
   move => B [x] [r] ->.
   rewrite openE -!ball_normE /interior=> y /= bxy.
@@ -888,7 +880,7 @@ rewrite -nbhs_ballE  /nbhs_ball /nbhs_ball_ /filter_from //=.
 move=> [r] r0 Bxr /=.
 rewrite nbhs_simpl /=; exists (ball x r) => //; split; last by apply: ballxx.
 by exists x; exists r.
-Admitted.
+Qed.
 
 HB.instance Definition _ :=
  Uniform_isTvs.Build K V add_continuous
@@ -6128,3 +6120,4 @@ by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j.
 Qed.
 
 End vitali_lemma_infinite.
+
diff --git a/theories/tvs.v b/theories/tvs.v
index 305e0b2980..e09b1ba9f0 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -41,7 +41,7 @@ HB.structure Definition UniformLmodule (K : numDomainType) :=
 
 Definition convex (R : numDomainType) (M : lmodType R) (A : set M) :=
   forall x y (lambda : R), x \in A -> y \in A -> 
-  (`|lambda| < 1) -> lambda *: x + (1 - lambda) *: y \in A.
+  (0< lambda) -> (lambda < 1) -> lambda *: x + (1 - lambda) *: y \in A.
 
 HB.mixin Record Uniform_isTvs (R : numDomainType) E of Uniform E & GRing.Lmodule R E := {
   add_continuous : continuous (fun x : E * E => x.1 + x.2) ;