From 4a402fb26f9f5a094e36718a515222063ba2b43a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 31 Oct 2025 05:36:21 +0900 Subject: [PATCH 1/2] fixes #1735 --- theories/sequences.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index 491d379167..e90daf49cb 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -57,7 +57,7 @@ From mathcomp Require Import ereal topology tvs normedtype landau. (* is convergent and its limit is sup u_n *) (* nonincreasing_cvgn u_ == if u_ is nonincreasing u_ and bound by below *) (* then u_ is convergent *) -(* adjacent == adjacent sequences lemma *) +(* adjacent_seq == adjacent sequences lemma *) (* cesaro == Cesaro's lemma *) (* ``` *) (* *) @@ -681,7 +681,7 @@ rewrite -(opprK u_); apply: is_cvgN; apply/(@near_nondecreasing_is_cvgn _ (- m)) - by apply: filterS u_m => x u_x; rewrite lerNl opprK. Qed. -Lemma adjacent (u_ v_ : R ^nat) : nondecreasing_seq u_ -> nonincreasing_seq v_ -> +Lemma adjacent_seq (u_ v_ : R ^nat) : nondecreasing_seq u_ -> nonincreasing_seq v_ -> v_ - u_ @ \oo --> 0 -> [/\ limn v_ = limn u_, cvgn u_ & cvgn v_]. Proof. @@ -699,6 +699,8 @@ by split=> //; apply/eqP; rewrite -subr_eq0 -limB //; exact/eqP/cvg_lim. Qed. End sequences_R_lemmas. +#[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `adjacent_seq`")] +Notation adjacent := adjacent_seq (only parsing). Definition harmonic {R : fieldType} : R ^nat := [sequence n.+1%:R^-1]_n. Arguments harmonic {R} n /. From fe6f4c6602d85c6ed3e4596e939384a7b19c4572 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 31 Oct 2025 05:37:43 +0900 Subject: [PATCH 2/2] changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 344dcb5ba2..cc030bb6b0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -339,6 +339,9 @@ + `lb_ereal_inf` -> `le_ereal_inf_tmp` + `ereal_sup_ge` -> `le_ereal_sup_tmp` +- in `sequences.v`: + + `adjacent` -> `adjacent_seq` + ### Generalized - in `pseudometric_normed_Zmodule.v`: