clean

Author: mkerjean

theories/normedtype_theory/tvs.v

@@ -752,14 +752,11 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
     entourage_inv entourage_split_ex
     nbhsE.
 
-(* TO BE DELETED once PR#1974 is merged *)
-
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous.
 
 HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous.
 
 HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex.
-(* END TO BE DELETED *)
 
 HB.end.
 
@@ -777,7 +774,7 @@ Lemma addset0 (E : zmodType) (A: set E):
  ([set 0] `+ A) = A.
 Proof.
 apply/seteqP; split => z /=.
-  by move=> [+ -> [y]]; rewrite add0r => + + <-. 
+  by move=> [+ -> [y]]; rewrite add0r => + + <-.
 by move=> Az; exists 0 => //; exists z; rewrite ?add0r.
 Qed.
 
@@ -927,93 +924,60 @@ have [convV'' balV''] := (absconvex_nbhsbasisat0 fV0 ).
 exists ((ball_ normr 0 (minr 1 s)) (*[set t | `|t| < r]*), [set x] `+ V0) => //=.
   split.
    exists (minr 1 s) => //=. rewrite /minr; case: ifPn => //.
-   by rewrite r0.
+     by rewrite r0.
    by exists ([set x] `+ V0) => //; exists V0.
-move => [z1 z2] /=.
-rewrite sub0r normrN => -[z1s].
-move=> [_ ->] [y] Vy <- {z2}.
-apply: VA => /=.
-rewrite r0; exists 0.
-rewrite scale0r //.
+move => [z1 z2] /=; rewrite sub0r normrN => -[z1s].
+move=> [_ ->] [y] Vy <- {z2}; apply: VA => /=; rewrite r0; exists 0; rewrite ?scale0r //.
 exists (z1 *: (x + y)); rewrite ?add0r //.
-apply: rV0 => /=.
-exists (z1 *: x).
- apply: (balV'' (z1 * s^-1)). 
-  rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //.  
-  rewrite mul1r.
-  rewrite [ltRHS]gtr0_norm //.  
-  rewrite (lt_le_trans z1s) //. 
-  by rewrite /minr; case: ifPn => // /ltW //. 
-  exists (s *: x) => //.
-  by  rewrite !scalerA divfK//  gt_eqF //.
-exists (z1 *: y) => //.
-  apply: (balV'' z1).
-  rewrite (le_trans (ltW z1s)) //. 
-  rewrite /minr; case: real_ltP => //.
-  rewrite gtr0_real //.  
-  by exists y.
-by rewrite -scalerDr.
-
+apply: rV0 => /=; exists (z1 *: x).
+  apply: (balV'' (z1 * s^-1)).
+    rewrite normrM normfV ltW // ltr_pdivrMr ?normr_gt0 ?gt_eqF //.
+    rewrite mul1r [ltRHS]gtr0_norm // (lt_le_trans z1s) //.
+    by rewrite /minr; case: ifPn => // /ltW //.
+  by exists (s *: x) => //; rewrite !scalerA divfK// gt_eqF //.
+exists (z1 *: y) => //; last by rewrite -scalerDr.
+apply: (balV'' z1); last by exists y.
+rewrite (le_trans (ltW z1s)) // /minr; case: real_ltP => //;
+by rewrite gtr0_real.
 have [V0 fV0 rV0] := (split_nbhsbasisat0 fV).
 have [V' fV' rV'] := (split_nbhsbasisat0 fV0).
-have [V'' fV'' rV''] := (expand_nbhsbasisat0 r fV'). 
-have [/= s [s0 (*xV'' xx'*)]] := (absorbing_nbhsbasisat0 fV'' x). 
+have [V'' fV'' rV''] := (expand_nbhsbasisat0 r fV').
+have [/= s [s0 (*xV'' xx'*)]] := (absorbing_nbhsbasisat0 fV'' x).
 rewrite inE => xV''.
-have [convV'' balV''] := (absconvex_nbhsbasisat0 fV''). 
-exists ([set r] `+ (ball_ normr 0 (Num.min `|r| (`|r * s|))) (*[set t | `|t| < r]*), [set x] `+ V'') => //=.
-  split. 
-    exists ((Num.min `|r| (`|r * s|))) => //=.
-      rewrite /minr; case: ifPn.  rewrite normr_gt0 //.
-      rewrite normr_gt0 => _. 
-      by rewrite mulf_neq0 // gt_eqF.
-    move=> u/= rur.
-    exists r => //.
-    exists (u - r).
-      rewrite sub0r normrN distrC (lt_le_trans rur)//. 
-    by rewrite subrKC.
-  by exists ([set x] `+ V'') => //; exists V''.
-move => [z1 z2] /= => [] [[x0] -> {x0}] [y]. 
-rewrite add0r normrN => yr. 
-move => <- [H ->] [t] Vt <-. 
-apply: VA => /=.
-exists (r *: x) => //.
-exists (r *: t + y *: x + y *: t) => //.
-  apply: rV0 => /=. 
-  exists (r *:t) => //. 
-    apply: rV'. exists 0. apply: mem0_nbhsbasisat0 =>//. exists (r *: t). apply: rV''. exists t => //.
-    by rewrite add0r.
-  exists  (y *: x + y *: t)=> //.
-    apply: rV'.
-      exists (y *: x).
-        apply: rV''.
-        exists ((r^-1 * y) *: x).  
-          apply: (balV'' (r^-1 * y * s^-1)).
-          rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1.
-          rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0 //.
-          rewrite (le_trans (ltW yr)) //; rewrite /minr.
-          case: ifPn => //. move/ltW. rewrite normrM normfV //.  
-          by rewrite invrK //.
-          by move=> _; rewrite normfV normrM invrK.     
-         exists (s *: x) => //.
-     rewrite !scalerA divfK//  gt_eqF //. 
-     by rewrite scalerA mulrA divff// mul1r.
-    exists (y *: t) => //.
-    apply: rV''.
-    exists ((r^-1 * y) *: t).
-      apply: (balV'' (r^-1 * y)).
-        rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1. 
-        apply: (le_trans (ltW yr)). 
-        rewrite /minr.  
-        case : real_ltP => //. 
-      by exists t.
-    by rewrite scalerA mulrA divff// mul1r.
-  by rewrite addrA.
-rewrite !addrA.
-rewrite -scalerDr.
-rewrite -addrA.
-rewrite -scalerDr.
-by rewrite scalerDl.
-Qed. 
+have [convV'' balV''] := (absconvex_nbhsbasisat0 fV'').
+exists ([set r] `+ (ball_ normr 0 (Num.min `|r| (`|r * s|))) , [set x] `+ V'') => //=.
+  split; last  by exists ([set x] `+ V'') => //; exists V''.
+  exists ((Num.min `|r| (`|r * s|))) => //=.
+  rewrite /minr; case: ifPn; first by rewrite normr_gt0 //.
+    by rewrite normr_gt0 => _ ; rewrite mulf_neq0 // gt_eqF.
+  move=> u/= rur; exists r => //; exists (u - r); last by rewrite subrKC.
+  by rewrite sub0r normrN distrC (lt_le_trans rur)//.
+move => [z1 z2] /= => [] [[x0] -> {x0}] [y]; rewrite add0r normrN => yr.
+move => <- [H ->] [t] Vt <-; apply: VA => /=.
+exists (r *: x) => //; exists (r *: t + y *: x + y *: t); last first.
+  by rewrite !addrA -scalerDr -addrA -scalerDr scalerDl.
+apply: rV0; exists (r *:t) => //.
+  apply: rV'; exists 0; first by apply: mem0_nbhsbasisat0.
+  exists (r *: t); first by apply: rV''; exists t.
+  by rewrite add0r.
+exists (y *: x + y *: t); last by rewrite addrA.
+apply: rV'; exists (y *: x).
+apply: rV''.
+   exists ((r^-1 * y) *: x).
+      apply: (balV'' (r^-1 * y * s^-1)).
+      rewrite -mulrA normrM normfV // ler_pdivrMl ?normr_gt0 // mulr1.
+      rewrite normrM -ler_pdivlMr ?normr_gt0 // ?gt_eqF // ?invr_gt0 //.
+      rewrite (le_trans (ltW yr)) //; rewrite /minr.
+      case: ifPn; last by move=> _; rewrite normfV normrM invrK.
+      by move/ltW; rewrite normrM normfV invrK.
+   exists (s *: x); rewrite // !scalerA divfK//  gt_eqF //.
+   by rewrite scalerA mulrA divff// mul1r.
+exists (y *: t) => //;  apply: rV''; exists ((r^-1 * y) *: t); last first.
+  by rewrite scalerA mulrA divff// mul1r.
+apply: (balV'' (r^-1 * y)); last by exists t.
+rewrite normrM normfV// ler_pdivrMl ?normr_gt0// mulr1.
+by apply: (le_trans (ltW yr)); rewrite /minr; case : real_ltP.
+Qed.
 
 #[local] Lemma locally_convex : exists2 B : set_system E,
     (forall b, b \in B -> absolutely_convex_set b) & nbhs_basis 0 B.
@@ -1022,43 +986,12 @@ exists nbhsbasis_at0; first by move=> b; rewrite inE; apply: absconvex_nbhsbasis
 move => b [a] /= [a'] fa; rewrite addset0 => <- ab /=.
 by exists a' => //=; split => //; exact: mem0_nbhsbasisat0.
 Qed.
- 
+
 HB.instance Definition _ := @PreTopologicalLmod_isConvexTvs.Build R E add_continuous scale_continuous locally_convex.
 
 HB.end.
-(*
- nbhsbasis_at0 : set_system E ; (*TODO rename to filterbasis_at0*)
-  nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U;
-  nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V ->
-    exists2 W, nbhsbasis_at0 W & W `<=` U `&` V ;
-  mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0 ;
-  expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B -> (*0 <= r ->*)
-    exists2 U, nbhsbasis_at0 U & r `*: U `<=` B ; (* implies circled *)
-  absorbing_nbhsbasisat0 : forall B , nbhsbasis_at0 B -> pabsorbing_set B;
-  absconvex_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> absolutely_convex_set B }.
 
-*)
-(* TB renamed *)
-Lemma nbhsbasisat0_filter (R : numFieldType) (E : lmodType R)
-    (nbhsbasis_at0 : set_system E) (x : E)
-(nonempty_nbhsbasisat0 : exists U, nbhsbasis_at0 U)
-( nbhsbasis_at0I : forall U V, nbhsbasis_at0 U -> nbhsbasis_at0 V -> exists2 W, nbhsbasis_at0 W & W `<=` U `&` V )
-(mem0_nbhsbasisat0 : forall B, nbhsbasis_at0 B -> B 0) :  ProperFilter (@nbhs_frombasis0 R E (nbhsbasis_at0) x).
-Proof.
-apply: filter_from_proper.
-  apply: filter_from_filter => /=.
-  have [U fU] := nonempty_nbhsbasisat0.
-  by exists ([set x] `+ U) => //=; exists U.
-  move=> _ _ /= [U0 FU <-] [V0 FV <-].
-  have [W FW WUV] := nbhsbasis_at0I _ _ FU FV.
-  exists ([set x] `+ W); first by exists W.
-  rewrite -addsetI; exact: addsubset.
-move=> _ /= [V FV]  <-.
-by exists x; exists x => //; exists 0; rewrite ?addr0//; exact: mem0_nbhsbasisat0.
-Qed.
-
-
-HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E (*& isConvexTvsat R E*) := {
+HB.factory Record Nbhssubbasis0_isConvexTvs (R: numFieldType) E & GRing.Lmodule R E := {
   nbhssubbasis0 : set_system E ;
   nonempty_nbhssubbasisat0 : exists U, nbhssubbasis0 U;
   mem0_nbhssubbasisat0 : forall B, nbhssubbasis0 B -> B 0 ;
@@ -1071,11 +1004,9 @@ Definition nbhs_fromsubbasis0 (R : numFieldType) (E : zmodType)
     (nbhssubbasis0 : set_system E)  :=
   finI_from nbhssubbasis0 id.
 
-
 HB.builders Context R E & Nbhssubbasis0_isConvexTvs R E.
 
 From mathcomp Require Import finmap.
-(*Open Scope fset_scope.  *)
 
 Let nbhsbasis_at0 := @nbhs_fromsubbasis0 R E nbhssubbasis0.
 
@@ -1109,7 +1040,6 @@ Proof.
 by move => B [/= I fI <-] U /= /fI /=; rewrite asboolE /= => /mem0_nbhssubbasisat0.
 Qed.
 
-
 #[local] Lemma expand_nbhsbasisat0 : forall B r, nbhsbasis_at0 B ->
   exists2 U, nbhsbasis_at0 U & r `*: U `<=` B.
 Proof.