convergence of a real function

- equivalence with convergent sequences

Co-authored-by: IshiguroYoshihiro <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -93,6 +93,9 @@
   + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
     `max_fun_continuous`.
 
+- in file `realfun.v`:
+  + lemma `cvg_nbhsP`
+
 ### Changed
 
 - in file `normedtype.v`,

theories/realfun.v

@@ -154,9 +154,9 @@ End fun_cvg_realFieldType.
 
 Section cvgr_fun_cvg_seq.
 Context {R : realType}.
+Implicit Types (f : R -> R) (p l : R).
 
-Lemma cvg_at_rightP (f : R -> R) (p l : R) :
-  f x @[x --> p^'+] --> l <->
+Lemma cvg_at_rightP f p l : f x @[x --> p^'+] --> l <->
   (forall u : R^nat, (forall n, u n > p) /\ (u n @[n --> \oo] --> p) ->
     f (u n) @[n --> \oo] --> l).
 Proof.
@@ -193,8 +193,7 @@ rewrite /sval/=; case: cid => // x [px xpn].
 by rewrite leNgt distrC => /negP.
 Unshelve. all: by end_near. Qed.
 
-Lemma cvg_at_leftP (f : R -> R) (p l : R) :
-  f x @[x --> p^'-] --> l <->
+Lemma cvg_at_leftP f p l : f x @[x --> p^'-] --> l <->
   (forall u : R^nat, (forall n, u n < p) /\ u n @[n --> \oo] --> p ->
     f (u n) @[n --> \oo] --> l).
 Proof.
@@ -207,8 +206,7 @@ apply: pfl.
 by split; [move=> k; rewrite ltrNl//|apply/cvgNP => /=; rewrite opprK].
 Qed.
 
-Lemma cvgr_dnbhsP (f : R -> R) (p l : R) :
-  f x @[x --> p^'] --> l <->
+Lemma cvgr_dnbhsP f p l : f x @[x --> p^'] --> l <->
   (forall u : R^nat, (forall n, u n != p) /\ (u n @[n --> \oo] --> p) ->
     f (u n) @[n --> \oo] --> l).
 Proof.
@@ -221,6 +219,38 @@ apply: cvg_at_right_left_dnbhs.
 - by apply/cvg_at_leftP => u [pu ?]; apply: pfl; split => // n; rewrite lt_eqF.
 Unshelve. all: end_near. Qed.
 
+Lemma cvg_nbhsP f p l : f x @[x --> p] --> l <->
+  (forall u : R^nat, (u n @[n --> \oo] --> p) -> f (u n) @[n --> \oo] --> l).
+Proof.
+split=> [/cvgrPdist_le /= fpl u /cvgrPdist_lt /= uyp|pfl].
+  apply/cvgrPdist_le => e /fpl[d d0 pdf].
+  by apply: filterS (uyp d d0) => t /pdf.
+apply: contrapT => fpl; move: pfl; apply/existsNP.
+suff: exists2 x : R ^nat,
+    x n @[n --> \oo] --> p & ~ f (x n) @[n --> \oo] --> l.
+  by move=> [x_] hp; exists x_; exact/not_implyP.
+have [e He] : exists e : {posnum R}, forall d : {posnum R},
+    exists xn, `|xn - p| < d%:num /\ `|f xn - l| >= e%:num.
+  apply: contrapT; apply: contra_not fpl => /forallNP h.
+  apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0).
+  move/forallNP => {}h; near=> t.
+  have /not_andP[abs|/negP] := h t.
+  - exfalso; apply: abs.
+    by near: t; exists d%:num => //= z/=; rewrite distrC.
+  - by rewrite -ltNge distrC => /ltW.
+have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
+exists (fun n => sval (cid (He (PosNum (invn n))))).
+  apply/cvgrPdist_lt => r r0; near=> t.
+  rewrite /sval/=; case: cid => x [xpt _].
+  rewrite distrC (lt_le_trans xpt)// -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//.
+  near: t; exists `|ceil r^-1|%N => // s /=.
+  rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans.
+  by rewrite natr_absz gtr0_norm -?ceil_gt0 ?invr_gt0 ?le_ceil ?num_real.
+move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
+rewrite /sval/=; case: cid => // x [px xpn].
+by rewrite ltNge distrC => /negP.
+Unshelve. all: end_near. Qed.
+
 End cvgr_fun_cvg_seq.
 
 Section cvge_fun_cvg_seq.