From 33abd4c082eb761a92361c904e2c58a7ef097b0f Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Sun, 27 Apr 2025 16:11:05 +0900 Subject: [PATCH 1/3] add Lemma cvge_ninftyP --- theories/realfun.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/theories/realfun.v b/theories/realfun.v index 4001c69ff..4a7162270 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -374,6 +374,19 @@ move /not_near_inftyP => eps_sep; exists (PosNum eps_gt0) => A /=. by case: (eps_sep _ (num_real A)) => x ? ?; exists x. Unshelve. all: by end_near. Qed. +(* NB: almost the same proof as cvg_ninftyP *) +Lemma cvge_ninftyP (f : R -> \bar R) (l : \bar R) : + f x @[x --> -oo] --> l <-> + forall u : R^nat, (u n @[n --> \oo] --> -oo) -> f (u n) @[n --> \oo] --> l. +Proof. +rewrite cvgNy_compNP cvge_pinftyP/= (@bij_forall R^nat _ -%R)//. +have u_opp (u : R^nat) : + ((- u) n @[n --> \oo] --> +oo) = (u n @[n --> \oo] --> -oo). + by rewrite propeqE cvgNry. +by under eq_forall do + (rewrite u_opp; under (eq_cvg _ (nbhs l)) do rewrite opprK). +Qed. + End cvge_fun_dvg_seq. Section fun_cvg_realType. From 7126b1d780bee47a69b67b54395f414bd37c8422 Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Sun, 27 Apr 2025 16:16:13 +0900 Subject: [PATCH 2/3] add to CHANGELOG --- CHANGELOG_UNRELEASED.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 45cceda03..559a38e06 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,6 +36,8 @@ - in `exp.v`: + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1` + Instance `is_derive1_powR` +- in `realfun.v`: + + lemma `cvge_ninftyP` ### Changed From e6d8d3dd6f7f61998bfb09eea36b4f82e85a7ad4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 30 Apr 2025 15:07:01 +0900 Subject: [PATCH 3/3] fix --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 559a38e06..c4392181d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -37,7 +37,7 @@ + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1` + Instance `is_derive1_powR` - in `realfun.v`: - + lemma `cvge_ninftyP` + + lemma `cvge_ninftyP` ### Changed