make not_near_at_right/left equivalence (#1445)

* make not_near_at_right/left equivalence --------- Co-authored-by: amethyst <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]>
math-comp · Jan 13, 2025 · 3cff9bb · 3cff9bb
1 parent 317c05c
commit 3cff9bb
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 10 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -30,6 +30,9 @@
 - in `classical_sets.v`:
   + lemmas `xsectionE`, `ysectionE`
 
+- in `normedtype.v`:
+  + lemma `nbhs_right_leftP`
+
 ### Changed
 
 - in `lebesgue_integrale.v`
@@ -78,6 +81,9 @@
     `is_cvg_nneseries`, `is_cvg_npeseries`, `nneseries_ge0`, `npeseries_le0`,
     `lee_nneseries`
 
+- in `normedtype.v`:
+  + lemmas `not_near_at_rightP`, `not_near_at_leftP`
+
 ### Deprecated
 
 ### Removed

diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -1329,6 +1329,13 @@ rewrite !near_withinE !near_simpl nbhs0P; split=> Px.
 by rewrite -oppr0 nearN; near=> e; rewrite gtrDl oppr_lt0; apply: (near Px).
 Unshelve. all: by end_near. Qed.
 
+Lemma nbhs_right_leftP (p : R) (P : pred R) :
+  (\forall x \near (- p)^'+, (P \o -%R) x) <-> (\forall x \near p^'-, P x).
+Proof.
+by rewrite nbhs_right0P nbhs_left0P; split;
+  apply: filterS=> r/=; rewrite opprD opprK.
+Qed.
+
 Lemma nbhs_right_gt x : \forall y \near x^'+, x < y.
 Proof. by rewrite near_withinE; apply: nearW. Qed.
 
@@ -1375,7 +1382,8 @@ by apply: nbhs_right_lt; rewrite subr_gt0.
 Unshelve. all: by end_near. Qed.
 
 Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y.
-Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt.
+Proof.
+by move=> xz; near do apply/ltW; apply: nbhs_left_gt.
 Unshelve. all: by end_near. Qed.
 
 Lemma nbhs_left_ltBl x e : 0 < e -> \forall y \near x^'-, x - y < e.
@@ -1415,23 +1423,32 @@ rewrite (@fun_predC _ -%R)/=; last exact: opprK.
 by rewrite image_id; under eq_fun do rewrite ltrNl opprK.
 Qed.
 
+(* NB: In not_near_at_rightP (and not_near_at_rightP), R has type numFieldType.
+  It is possible realDomainType could make the proof simpler and at least as
+  useful. *)
 Lemma not_near_at_rightP (p : R) (P : pred R) :
-  ~ (\forall x \near p^'+, P x) ->
+  ~ (\forall x \near p^'+, P x) <->
   forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P x.
 Proof.
-move=> pPf e; apply: contrapT => /forallPNP peP; apply: pPf; near=> t.
-apply: contrapT; apply: peP; apply/andP; split.
-- by near: t; exact: nbhs_right_gt.
-- by near: t; apply: nbhs_right_lt; rewrite ltrDl.
+split=> [pPf e|ex_notPx].
+- apply: contrapT => /forallPNP peP; apply: pPf; near=> t.
+  apply: contrapT; apply: peP; apply/andP; split.
+  + by near: t; exact: nbhs_right_gt.
+  + by near: t; apply: nbhs_right_lt; rewrite ltrDl.
+- rewrite /at_right near_withinE nearE.
+  rewrite -filter_from_ballE /filter_from/= -forallPNP => _ /posnumP[d].
+  have [x /andP[px xpd] notPx] := ex_notPx d; rewrite -existsNP; exists x => /=.
+  apply: contra_not notPx; apply => //.
+  by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
 Unshelve. all: by end_near. Qed.
 
 Lemma not_near_at_leftP (p : R) (P : pred R) :
-  ~ (\forall x \near p^'-, P x) ->
+  ~ (\forall x \near p^'-, P x) <->
   forall e : {posnum R}, exists2 x : R, p - e%:num < x < p & ~ P x.
 Proof.
-move=> pPf e; have := @not_near_at_rightP (- p) (P \o -%R).
-rewrite at_rightN => /(_ _ e)[|x pxe Pfx]; first by rewrite filterN.
-by exists (- x) => //; rewrite ltrNl ltrNr opprB addrC andbC.
+rewrite -nbhs_right_leftP not_near_at_rightP; split => + e => /(_ e)[r pre Pr].
+- by exists (- r) => //; rewrite ltrNr andbC ltrNl opprB addrC.
+- by exists (- r) => /=; rewrite ?opprK// ltrN2 ltrNl opprD opprK andbC.
 Qed.
 
 End at_left_right.