From ca3fb2d5c1087996bba36ddd814382cab1e6ceb3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 15 Nov 2024 00:30:46 +0900 Subject: [PATCH] convergence of a real function - equivalence with convergent sequences Co-authored-by: IshiguroYoshihiro --- CHANGELOG_UNRELEASED.md | 3 +++ theories/realfun.v | 42 +++++++++++++++++++++++++++++++++++------ 2 files changed, 39 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 56017a4e2..7cd2337fc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -35,6 +35,9 @@ - in `probability.v` + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed) +- in `realfun.v`: + + lemma `cvgr_nbhsP` + ### Changed - in `lebesgue_integrale.v` diff --git a/theories/realfun.v b/theories/realfun.v index 5028c4d1b..b5ade1781 100644 --- a/theories/realfun.v +++ b/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 cvgr_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.