proofs

theories/normedtype.v

@@ -804,7 +804,9 @@ HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldTyp
 }.
 
 HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
-(* These lemmas are done latter with more machinery. Move the factory ?*)
+
+
+(* These lemmas are done latter with more machinery. Can we move this factory down ?*)
 Lemma add_continuous : continuous (fun x : V * V => x.1 + x.2).
 Proof.
 move=> [/= x y]; apply/cvg_ballP => e e0 /=.
@@ -814,33 +816,66 @@ rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0.
 rewrite -ball_normE /= /ball_ /= => xy /= [nx ny].
 rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (@splitr K (e)) ltrD //=.
 Qed.
-
+ 
 Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2).
 Proof.
-move=> [/= k x]; apply/cvg_ballP => e e0 /=.
+move=> [/= k x].
+apply/cvg_ballP => e e0 /=.
 rewrite nearE /= -nbhs_ballE  /nbhs_ball /nbhs_ball_ //=.
-near +oo_K => M.
-pose r := (e/2/M).
+near +oo_K=> M.
+pose r := (`|e|/2/M).
 exists ((ball k r),(ball x r)).
-rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0.
-rewrite -ball_normE /= /ball_ /= => lz /= [nk nx].
-rewrite -?(scalerBr, scalerBl).
-have := @ball_split _ _ (k *: lz.2)  (k*: x)  (lz.1 *: lz.2) e; rewrite -ball_normE /=.
-move => T; apply: T; rewrite -?(scalerBr, scalerBl) normrZ.
-  by rewrite (@le_lt_trans _ _ (M * `|x - lz.2|)) ?ler_wpM2r -?ltr_pdivlMl// mulrC.
+rewrite !nbhs_simpl /=; split; apply: nbhsx_ballx; rewrite ?divr_gt0 // ?normr_gt0 ?lt0r_neq0 //.
+rewrite -ball_normE /= /ball_ /= => lz /= [nk nx]. 
+rewrite -?(scalerBr, scalerBl). 
+have := @ball_split _ _ (k *: lz.2)  (k*: x)  (lz.1 *: lz.2) `|e|; rewrite -ball_normE /= real_lter_normr ?gtr0_real //. 
+have -> :  (normr (k *: x - lz.1 *: lz.2) < - e) = false by rewrite ltr_nnorml // oppr_le0 ltW.
+rewrite Bool.orb_false_r => T;apply: T; rewrite -?(scalerBr, scalerBl) normrZ. 
+rewrite (@le_lt_trans _ _ (M * `|x - lz.2|)) ?ler_wpM2r -?ltr_pdivlMl //  mulrC //.
 rewrite (@le_lt_trans _ _ (`|k - lz.1| * M)) ?ler_wpM2l -?ltr_pdivlMr//.
- near: M. admit.
+rewrite (@le_trans _ _ (normr (lz.2) + normr x)) // ?lerDl ?normr_ge0 //.
+move: nx; rewrite /r => nx. 
+have H: normr lz.2 <= normr x + `|e|/2/M.
+   have -> : lz.2 = x - (x -lz.2) by rewrite opprB addrCA subrr addr0.
+   by rewrite (@le_trans _ _ (normr (x) + normr (x - lz.2))) // ?ler_normB // ?lerD // ltW //.
+rewrite (@le_trans _ _ ((normr x + `|e| / 2 / M) + (normr x))) // ?lerD //.
+rewrite addrAC.
+have H0: M = M^-1 * (M *  M). rewrite mulrA mulVf ?mul1r // ?lt0r_neq0 //.
+rewrite [X in (_ <= X)]H0.
+have -> :   (normr x + normr x + `|e| / 2 / M) =   M^-1 *  ( M* (normr x + normr x)  + `|e| / 2).
+   by rewrite mulrDr mulrA mulVf ?mul1r  ?lt0r_neq0 // mulrC.
+rewrite  ler_wpM2l // ?invr_ge0 // ?ltW // -ltrBrDl -mulrBr. 
+apply: ltr_pM; rewrite ?ltrBrDl //.
 Unshelve. all: by end_near.
-Admitted.
+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 zy l1.
-  rewrite opprD scalerDl opprD.
-  rewrite scale1r [X in (_ + X)]addrC addrA [X in (X - _)]addrA.
-  rewrite scaleNr opprK -addrA. admit.
+  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 -> :
+  (l *: x + (1 - l) *: x) - (l *: z + (1 - l) *: y) = (l *: (x-z) + (1 - l) *: (x - y)).
+  rewrite opprD. rewrite addrCA.  admit.
+  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.
 split =>  /=.
   move => B [x] [r] ->.
   rewrite openE -!ball_normE /interior=> y /= bxy.
@@ -900,7 +935,7 @@ Variable (R : rcfType).
 HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
-#[export, non_forgetful_inheritance]
+ #[export, non_forgetful_inheritance]
 HB.instance Definition _ := NormedModule.copy R R^o.
 End rcfType.