wip entourage evt

Author: mkerjean

theories/evt.v

@@ -100,7 +100,20 @@ HB.builders Context R E of TopologicalLmod_isEvt R E.
     Unshelve. all: by end_near.
   Qed.
 
-  
+  Lemma nbhs_scaler: forall (U : set E) (r : R) (x :E),  (
+    r != 0) -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U).
+  Proof.
+    move => U r x r0 U0; move: (@scale_continuous ((r^-1,r *:x)) U).
+    rewrite /= scalerA mulrC divrr ?scale1r ?unitfE //= =>/(_ U0).
+    case=>//= [B] [B1 B2] BU.
+    near=> z => //=.
+    exists (r^-1*:z).
+    apply: (BU (r^-1,z)); split => //=; last by near: z.
+    by apply: nbhs_singleton.
+    by rewrite scalerA divrr ?scale1r ?unitfE //=.
+    Unshelve. all: by end_near.
+  Qed.
+
   Lemma nbhsT: forall (U : set E), forall (x : E), nbhs 0 U -> nbhs x (+%R x @`U).
   Proof.
   move => U x U0. 
@@ -154,30 +167,39 @@ HB.builders Context R E of TopologicalLmod_isEvt R E.
 
 Lemma nbhsE_subproof : nbhs = nbhs_ entourage.
 Proof.
+have lem: (-1 != (0 : R)) by rewrite oppr_eq0 oner_eq0.
 rewrite /nbhs_  /=; apply: funext => x; rewrite /filter_from /=.
 apply: funext => U; apply: propext => /=; rewrite /entourage /=; split.
-move=> nU; exists [set xy | U(x  + (xy.1 - xy.2))].
-  exists ((fun z => z-x) @` U); split.
-    rewrite -(addrN x) addrC; move: (nbhs_add (-x) nU).
-    have -> : [set ((- x)%R + x0)%E | x0 in U] = [set z - x | z in U].
-      apply: funext => z /=; apply: propext; split;
-      by move=> [x0 U0]; rewrite addrC=> H; exists x0.
-    by [].
-  move => xy; rewrite !inE /= => [[z] Uz ] <-.
-  by rewrite addrCA subrr addr0.
-move => /= z. (*issue*) admit.
+  pose V := [set v | (x-v) \in U] : set E.
+  move=> nU; exists [set xy |  (xy.1 - xy.2) \in V]. 
+    exists V;split.
+      move: (nbhs_add (x) (nbhs_scaler lem nU))=> /=.
+      rewrite scaleN1r subrr /= /V.
+      have -> : [set (x + x0)%E | x0 in [set -1 *: x | x in U]] 
+                = [set v | x - v \in U].
+       apply: funext => /= v /=; rewrite inE; apply: propext; split.
+         by move => [x0 [x1]] Ux1 <- <-; rewrite scaleN1r opprB addrCA subrr addr0.  
+      move=> Uxy. exists (v - x). exists (x -v) => //.
+      by rewrite scaleN1r opprB.
+      by rewrite addrCA subrr addr0 //. 
+      by [].
+    by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE.
+  by move=> y; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE.
 move=> [A [U0 [NU UA]] H].
 near=> z; apply: H => /=; rewrite -inE; apply: UA => /=.
 near: z; rewrite nearE.
-move: (nbhsT x NU)=> /=.
-have -> : [set (x + x0)%E | x0 in U0] = (fun x0 : E => x - x0 \in U0).
- apply:funext => z /=; rewrite inE; apply: propext; split.
-  move=> [x0 H <-]; rewrite -opprB -addrAC addrN add0r.
-  admit (*issue*). 
-  move=> Uxz; exists (z-x). admit (*issue*). 
-  by rewrite addrCA subrr addr0.
+move: (nbhsT x (nbhs0_scaler lem NU))=> /=.
+have -> : 
+[set (x + x0)%E | x0 in [set -1 *: x | x in U0]] = (fun x0 : E => x - x0 \in U0).
+  apply:funext => /= z /=; apply: propext; split.
+    move=> [x0] [x1 Ux1 <-] <-.
+    rewrite  -opprB. rewrite addrAC subrr add0r inE scaleN1r opprK //.
+   rewrite inE => Uxz. exists (z-x). exists (x-z) => //.
+   by rewrite scalerBr !scaleN1r opprK addrC. 
+   by rewrite addrCA subrr addr0.
 by [].
-Admitted.
+Unshelve. all: by end_near.
+Qed.
 
 HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
     entourage_filter entourage_refl_subproof
@@ -203,7 +225,7 @@ Lemma add_continuousE (R : numDomainType) (E : evtType R):
 continuous (fun (xy : E*E )=> xy.1 + xy.2).
 Proof.
 apply: add_continuous.
-Admitted. 
+Qed.
 
 End bacasable.