From f76f0336d9b9f1507a2f1d7cb81758e9c04a1b48 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 28 Jul 2020 02:05:37 +0200 Subject: [PATCH] simplifications, extensions, generalizations, fixups, renamings --- CHANGELOG_UNRELEASED.md | 14 ++- theories/normedtype.v | 14 +++ theories/sequences.v | 189 ++++++++++++++++++---------------------- 3 files changed, 109 insertions(+), 108 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6ed3120ae1..fbd713a931 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -19,10 +19,14 @@ + arithmetic lemmas: `oppeD`, `subre_ge0`, `suber_ge0`, `lee_add2lE`, `lte_add2lE`, `lte_add`, `lte_addl`, `lte_le_add`, `lte_subl_addl`, `lee_subr_addr`, `lee_subl_addr`, `lte_spaddr` +- in `normedtype.v`, lemmas `natmul_continuous`, `cvgMn` and `is_cvgMn`. - in `sequences.v`: + definitions `arithmetic`, `geometric`, `geometric_invn` - + lemmas `mulrn_arithmetic`, `exprn_geometric`, `dvg_arithmetic`, `cvg_expr`, ` cvg_geometric_invn`, - `geometric_seriesE`, `cvg_geometric_series`, `is_cvg_geometric_series` + + lemmas `increasing_series`, `cvg_shiftS`, `mulrn_arithmetic`, + `exprn_geometric`, `cvg_arithmetic`, `cvg_expr`, + `geometric_seriesE`, `cvg_geometric_series`, + `is_cvg_geometric_series`. + + ### Changed @@ -156,6 +160,12 @@ + `derivable_locallyP` -> `derivable_nbhsP` + `derivable_locallyx` -> `derivable_nbhsx` + `derivable_locallyxP` -> `derivable_nbhsxP` +- in `sequences.v`, + + `cvg_comp_subn` -> `cvg_centern`, + + `cvg_comp_addn` -> `cvg_shiftn`, + + `telescoping` -> `telescope` + + `sderiv1_series` -> `seriesSB` + + `telescopingS0` -> `eq_sum_telescope` ### Removed diff --git a/theories/normedtype.v b/theories/normedtype.v index 99dda4b334..8497f242c5 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2759,6 +2759,14 @@ rewrite !near_simpl /=; near=> a b => /=; rewrite opprD addrACA. by rewrite normm_lt_split //; [near: a|near: b]; apply: cvg_dist. Grab Existential Variables. all: end_near. Qed. +Lemma natmul_continuous n : continuous (fun x : V => x *+ n). +Proof. +case: n => [|n] x; first exact: cvg_cst. +apply/cvg_distP=> _/posnumP[e]; rewrite !near_simpl /=; near=> a. +rewrite -mulrnBl normrMn -mulr_natr -ltr_pdivl_mulr//. +by near: a; apply: cvg_dist. +Grab Existential Variables. all: end_near. Qed. + Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). Proof. move=> [k x]; apply/cvg_distP=> _/posnumP[e]. @@ -2854,6 +2862,12 @@ Proof. by move=> /cvgN /cvgP. Qed. Lemma is_cvgNE f : cvg ((- f) @ F) = cvg (f @ F). Proof. by rewrite propeqE; split=> /cvgN; rewrite ?opprK => /cvgP. Qed. +Lemma cvgMn f n a : f @ F --> a -> ((@GRing.natmul _)^~n \o f) @ F --> a *+ n. +Proof. by move=> ?; apply: continuous_cvg => //; exact: natmul_continuous. Qed. + +Lemma is_cvgMn f n : cvg (f @ F) -> cvg (((@GRing.natmul _)^~n \o f) @ F). +Proof. by move=> /cvgMn /cvgP. Qed. + Lemma cvgD f g a b : f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b. Proof. by move=> ? ?; apply: continuous2_cvg => //; exact: add_continuous. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index d4860f25b5..6c4f13d058 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice seq. From mathcomp Require Import bigop div ssralg ssrint ssrnum fintype order. -From mathcomp Require Import binomial matrix interval rat. +From mathcomp Require Import binomial matrix interval rat zmodp. Require Import boolp reals ereal. Require Import classical_sets posnum topology normedtype landau derive forms. @@ -123,6 +123,8 @@ Local Notation eqolimPn := (@eqolimP _ _ _ eventually_filter). Section sequences_patched. (* TODO: generalizations to numDomainType *) +Section NatShift. + Variables (N : nat) (V : topologicalType). Implicit Types (f : nat -> V) (u : V ^nat) (l : V). @@ -142,7 +144,7 @@ by rewrite propeqE; split; [rewrite cvg_restrict|rewrite -(cvg_restrict f)] => /cvgP. Qed. -Lemma cvg_comp_subn u_ l : ([sequence u_ (n - N)%N]_n --> l) = (u_ --> l). +Lemma cvg_centern u_ l : ([sequence u_ (n - N)%N]_n --> l) = (u_ --> l). Proof. rewrite propeqE; split; last by apply: cvg_comp; apply: cvg_subnr. gen have cD : u_ l / u_ --> l -> (fun n => u_ (n + N)%N) --> l. @@ -150,13 +152,23 @@ gen have cD : u_ l / u_ --> l -> (fun n => u_ (n + N)%N) --> l. by move=> /cD /=; under [X in X --> l]funext => n do rewrite addnK. Qed. -Lemma cvg_comp_addn u_ l : ([sequence u_ (n + N)%N]_n --> l) = (u_ --> l). +Lemma cvg_shiftn u_ l : ([sequence u_ (n + N)%N]_n --> l) = (u_ --> l). Proof. rewrite propeqE; split; last by apply: cvg_comp; apply: cvg_addnr. -rewrite -[X in X -> _]cvg_comp_subn; apply: cvg_trans => /=. +rewrite -[X in X -> _]cvg_centern; apply: cvg_trans => /=. by apply: near_eq_cvg; near=> n; rewrite subnK//; near: n; exists N. Grab Existential Variables. all: end_near. Qed. +End NatShift. + +Variables (V : topologicalType). + +Lemma cvg_shiftS u_ (l : V) : ([sequence u_ n.+1]_n --> l) = (u_ --> l). +Proof. +suff -> : [sequence u_ n.+1]_n = [sequence u_(n + 1)%N]_n by rewrite cvg_shiftn. +by rewrite funeqE => n/=; rewrite addn1. +Qed. + End sequences_patched. Section sequences_R_lemmas_realFieldType. @@ -276,6 +288,7 @@ Section partial_sum. Variables (V : zmodType) (u_ : V ^nat). Definition series : V ^nat := [sequence \sum_(k < n) u_ k]_n. +Definition telescope : V ^nat := [sequence u_ n.+1 - u_ n]_n. Lemma seriesSr n : series n.+1 = series n + u_ n. Proof. by rewrite /series/= big_ord_recr/=. Qed. @@ -283,7 +296,7 @@ Proof. by rewrite /series/= big_ord_recr/=. Qed. Lemma seriesS n : series n.+1 = u_ n + series n. Proof. by rewrite addrC seriesSr. Qed. -Lemma sderiv1_series (n : nat) : series n.+1 - series n = u_ n. +Lemma seriesSB (n : nat) : series n.+1 - series n = u_ n. Proof. by rewrite seriesS addrK. Qed. Lemma seriesEord : series = [sequence \sum_(k < n) u_ k]_n. @@ -310,8 +323,20 @@ Proof. by rewrite sub_series_geq// -addnn leq_addl. Qed. End partial_sum. Arguments series {V} u_ n : simpl never. +Arguments telescope {V} u_ n : simpl never. Notation "[ 'series' E ]_ n" := (series [sequence E]_n) : ring_scope. +Lemma telescopeK (V : zmodType) (u_ : V ^nat) : + series (telescope u_) = [sequence u_ n - u_ 0%N]_n. +Proof. by rewrite funeqE => n; rewrite seriesEnat/= telescope_sumr. Qed. + +Lemma seriesK (V : zmodType) : cancel (@series V) telescope. +Proof. move=> ?; exact/funext/seriesSB. Qed. + +Lemma eq_sum_telescope (V : zmodType) (u_ : V ^nat) n : + u_ n = u_ 0%N + series (telescope u_) n. +Proof. by rewrite telescopeK/= addrC addrNK. Qed. + (* TODO: port to mathcomp *) (* missing mathcomp lemmas *) Lemma ler_sum_nat (R : numDomainType) (m n : nat) (F G : nat -> R) : @@ -410,7 +435,7 @@ Lemma near_nondecreasing_is_cvg (u_ : (R^o) ^nat) (M : R) : cvg u_. Proof. move=> [k _ u_nd] [k' _ u_M]; suff : cvg [sequence u_ (n + maxn k k')%N]_n. - by case/cvg_ex => /= l; rewrite cvg_comp_addn => ul; apply/cvg_ex; exists l. + by case/cvg_ex => /= l; rewrite cvg_shiftn => ul; apply/cvg_ex; exists l. apply (@nondecreasing_is_cvg _ M) => [/= ? ? ? | ?]. by rewrite u_nd ?leq_add2r ?(leq_trans (leq_maxl _ _) (leq_addl _ _))//. by rewrite u_M // (leq_trans (leq_maxr _ _) (leq_addl _ _)). @@ -524,17 +549,6 @@ Grab Existential Variables. all: end_near. Qed. End cesaro. -Definition telescoping (R : numDomainType) (u_ : R^o ^nat) := - [sequence u_ n.+1 - u_ n]_n. - -Lemma telescopingS0 (R : numDomainType) (u_ : R^o ^nat) n : - u_ n.+1 = u_ O + \sum_(i < n.+1) (telescoping u_) i. -Proof. -apply/eqP; rewrite addrC -subr_eq; apply/eqP. -elim: n => [|n ih]; first by rewrite big_ord_recl big_ord0 addr0. -by rewrite big_ord_recr /= -ih addrCA (addrC (u_ n.+1)) addrK. -Qed. - Section cesaro_converse. Variable R : archiFieldType. @@ -554,10 +568,10 @@ by rewrite lef_pinv // ?ler_nat // posrE // ltr0n. Grab Existential Variables. all: end_near. Qed. Lemma cesaro_converse (u_ : R^o ^nat) (l : R^o) : - telescoping u_ =o_\oo (harmonic) -> + telescope u_ =o_\oo harmonic -> arithmetic_mean u_ --> l -> u_ --> l. Proof. -pose a_ := telescoping u_ => a_o u_l. +pose a_ := telescope u_ => a_o u_l. suff abel : forall n, u_ n - arithmetic_mean u_ n = \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1. suff K : u_ - arithmetic_mean u_ --> (0 : R^o). @@ -572,7 +586,7 @@ suff abel : forall n, fun n => n.+1%:R^-1 * \sum_(k < n) k.+1%:R * a_ k); last first. rewrite funeqE => n; rewrite big_add1 /= big_mkord /= big_distrr /=. by apply eq_bigr => i _; rewrite mulrCA mulrA. - have {a_o}a_o : [sequence n.+1%:R * telescoping u_ n]_n --> (0 : R^o). + have {a_o}a_o : [sequence n.+1%:R * telescope u_ n]_n --> (0 : R^o). apply: (@eqolim0 R nat [normedModType R of R^o] eventually_filterType). rewrite a_o. set h := 'o_[filter of \oo] harmonic. @@ -587,10 +601,10 @@ case => [|n]. rewrite /arithmetic_mean /= invr1 mul1r /series /= big_ord_recl !big_ord0. by rewrite addr0 subrr big_nil. rewrite /arithmetic_mean /= /series /= big_ord_recl /=. -under eq_bigr do rewrite /bump /= add1n telescopingS0. +under eq_bigr do rewrite /bump /= add1n eq_sum_telescope. rewrite big_split /= big_const card_ord iter_addr addr0 addrA -mulrS mulrDr. rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA. -rewrite telescopingS0 (addrC (u_ O)) addrK. +rewrite eq_sum_telescope (addrC (u_ O)) addrK. rewrite [X in _ - _ * X](_ : _ = \sum_(0 <= i < n.+1) \sum_(0 <= k < n.+1 | (k < i.+1)%N) a_ k); last first. by rewrite big_mkord; apply eq_bigr => i _; rewrite big_mkord -big_ord_widen. @@ -626,13 +640,13 @@ End cesaro_converse. Section series_convergence. Lemma cvg_series_cvg_0 (K : numFieldType) (V : normedModType K) (u_ : V ^nat) : - cvg (series u_) -> u_ --> (0 : V^o). + cvg (series u_) -> u_ --> (0 : V). Proof. move=> cvg_series. rewrite (_ : u_ = fun n => series u_ (n + 1)%nat - series u_ n); last first. - by rewrite funeqE => i; rewrite addn1 sderiv1_series. + by rewrite funeqE => i; rewrite addn1 seriesSB. rewrite -(subrr (lim (series u_))). -by apply: cvgD; rewrite ?cvg_comp_addn//; apply: cvgN. +by apply: cvgD; rewrite ?cvg_shiftn//; apply: cvgN. Qed. Lemma nondecreasing_series (R : numFieldType) (u_ : R^o ^nat) : @@ -642,6 +656,13 @@ move=> u_ge0; apply: nondecreasing_seqP => n. by rewrite /series/= big_ord_recr ler_addl. Qed. +Lemma increasing_series (R : numFieldType) (u_ : R^o ^nat) : + (forall n, 0 < u_ n) -> increasing_seq (series u_). +Proof. +move=> u_ge0; apply: increasing_seqP => n. +by rewrite /series/= big_ord_recr ltr_addl. +Qed. + End series_convergence. Definition arithmetic (R : zmodType) a z : R^o ^nat := [sequence a + z *+ n]_n. @@ -656,99 +677,55 @@ Arguments geometric {R} a z n /. Lemma exprn_geometric (R : fieldType) : (@GRing.exp R) = geometric 1. Proof. by rewrite funeq2E => z n /=; rewrite mul1r. Qed. -Lemma dvg_arithmetic (R : realType) a (z : R^o) : +Lemma cvg_arithmetic (R : archiFieldType) a (z : R^o) : z > 0 -> arithmetic a z --> +oo. Proof. -move=> z0 /=; apply/cvgPpinfty => _ /posnumP[A]. -exists (`| (ifloor ((A%:num - a) / z) + 1)%R |%N) => // i. -rewrite -(@ler_nat [numDomainType of R]) => Hi. -rewrite -ler_subl_addl -mulr_natr -ler_pdivr_mull // mulrC (le_trans _ Hi) //. -case: (ltrP (A%:num - a) 0) => Aa0. - by rewrite (@le_trans _ _ 0) // pmulr_lle0 // ?invr_gt0 // ltW. -move: (ltW (floorS_gtr ((A%:num - a) / z))) => /le_trans; apply. -rewrite [X in X + _ <= _](floorE _) {2}(_ : 1 = 1%:~R) // -intrD. -rewrite -mulrz_nat ler_int -{1}(@gez0_abs (_ + _)) ?natz //. -by rewrite addr_ge0 // ifloor_ge0 divr_ge0 // ltW. -Qed. +move=> z_gt0; apply/cvgPpinfty => _ /posnumP[A]; near=> n => /=. +rewrite -ler_subl_addl -mulr_natl -ler_pdivr_mulr//; set x := (X in X <= _). +rewrite ler_normlW// ltW// (lt_le_trans (archi_boundP _))// ler_nat. +by near: n; apply: nbhs_infty_ge. +Grab Existential Variables. all: end_near. Qed. +(* Cyril: I think the shortest proof would rely on cauchy completion *) Lemma cvg_expr (R : archiFieldType) (z : R) : - 0 <= z < 1 -> (fun n => z ^+ n : R^o) --> (0 : R^o). -Proof. -case/andP; rewrite le_eqVlt => /orP[/eqP <- _ |z0 z1]. - apply/cvg_distP => _/posnumP[e]; rewrite near_map. - by exists 1%N => // n n0; rewrite sub0r normrN expr0n gtn_eqF // normr0. -pose t := 1%R - z. -have onezt : 1 = z + t by rewrite addrCA subrr addr0. -have t0 : 0 < t by rewrite subr_gt0. -apply (@squeeze _ _ (fun=> 0) _ (fun n => t^-1 * harmonic n)); last 2 first. - exact: (@cvg_cst [topologicalType of R^o]). - rewrite -(scaler0 _ t^-1); exact: (cvgZ (cvg_cst _) cvg_harmonic). -near=> n. -rewrite exprn_ge0 /= ?ler_pdivl_mull ?subr_gt0//; last exact: ltW. -rewrite -(mul1r (n.+1%:R)^-1) ler_pdivl_mulr ?ltr0n//. -move/(congr1 (fun x => x ^+ n.+1)) : onezt. -rewrite exprDn expr1n big_ord_recl subn0 expr0 bin0 mulr1n mulr1. -rewrite big_ord_recl subn1 expr1 bin1 addrCA => /eqP; rewrite -subr_eq => /eqP. -rewrite -mulr_natr mulrAC mulrC mulrA => <-; rewrite -subr_ge0 opprB addrCA. -rewrite subrr addr0 addr_ge0 // ?exprn_ge0//; first exact: ltW. -apply sumr_ge0 => i _; rewrite -mulr_natr mulr_ge0 // ?ler0n//. -by rewrite mulr_ge0 // ?exprn_ge0// ltW. + `|z| < 1 -> (@GRing.exp R z : R^o^nat) --> (0 : R^o). +Proof. +move=> Nz_lt1; apply: cvg_dist0; pose t := (1 - `|z|). +pose oo_filter := eventually_filterType. (* Cyril: fixme *) +apply: (@squeeze _ _ (cst 0) _ (t^-1 *: harmonic) oo_filter); last 2 first. +- exact: (@cvg_cst [topologicalType of R^o]). +- by rewrite -(scaler0 _ t^-1); exact: (cvgZr cvg_harmonic). +near=> n; rewrite normr_ge0 normrX/= ler_pdivl_mull ?subr_gt0//. +rewrite -(@ler_pmul2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl. +have -> : 1 = (`|z| + t) ^+ n.+1 by rewrite addrC addrNK expr1n. +rewrite exprDn (bigD1 (inord 1)) ?inordK// subn1 expr1 bin1 ler_addl sumr_ge0//. +by move=> i; rewrite ?(mulrn_wge0, mulr_ge0, exprn_ge0, subr_ge0)// ltW. Grab Existential Variables. all: end_near. Qed. -Definition geometric_invn {R : realFieldType} x : R^o ^nat := fun n => (x ^ n)%:R^-1. - -Lemma cvg_geometric_invn (R : archiFieldType) m : - (1 < m)%N -> geometric_invn m --> (0 : R^o). +Lemma geometric_seriesE (R : numFieldType) (a z : R) : z != 1 -> + series (geometric a z) = [sequence a * (1 - z ^+ n) / (1 - z)]_n. Proof. -move=> m1; rewrite (_ : geometric_invn _ = (fun n => (m%:R^-1) ^+n)); last first. - by rewrite funeqE => n; rewrite /geometric_invn natrX exprVn. -apply cvg_expr. -rewrite invr_ge0 ler0n /= invr_lt1 ?ltr1n// ?ltr0n ?(ltn_trans _ m1)//. -by rewrite unitfE pnatr_eq0 gt_eqF // ltEnat /= (leq_trans _ m1). +rewrite funeqE => z_neq1 n. +apply: (@mulIf _ (1 - z)); rewrite ?mulfVK ?subr_eq0 1?eq_sym//. +rewrite seriesEnat !mulrBr [in LHS]mulr1 mulr_suml -opprB -sumrB. +by under eq_bigr do rewrite -mulrA -exprSr; rewrite telescope_sumr// opprB. Qed. -Lemma geometric_seriesE (R : realFieldType) (a z : R) (n : nat) : z != 1 -> - series (geometric a z) n.+1 = a * (1 - z ^+ n.+1) / (1 - z). +Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 -> + series (geometric a z) --> (a * (1 - z)^-1 : R^o). Proof. -move=> z1; have ? : 1 - z \is a GRing.unit by rewrite unitfE subr_eq0 eq_sym. -apply: (@mulIr _ (1 - z)) => //; rewrite -!mulrA mulVr // mulr1 /series /=. -elim: n => [|n ih]. - by rewrite big_ord_recl big_ord0 expr0 mulr1 addr0 expr1. -rewrite big_ord_recr mulrDl {}ih -mulrA -mulrDr mulrBr mulr1. -by rewrite -exprSr addrA subrK. +move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//. +have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1. +by apply: cvgMl; apply: cvgMr; apply: cvgB; [apply: cvg_cst|apply: cvg_expr]. Qed. -Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : - 0 < z < 1 -> (series (geometric a z) --> (a * (1 - z)^-1 : R^o)). -Proof. -case/andP=> z0 z1. -have [/eqP ->|a0] := boolP (a == 0). - rewrite /series /geometric/= (_ : (fun _ => _) = (fun=> 0)). - by rewrite mul0r; exact: cvg_cst. - by rewrite funeqE => n; rewrite big1 //= => i _; rewrite mul0r. -rewrite /series. -apply/cvg_distP => _/posnumP[e]. -have ea1z_gt0 : (0%R < (e)%:num / `|a / (1 - z)|)%O. - rewrite divr_gt0 // normr_gt0 mulf_eq0 negb_or /= a0 invr_eq0 subr_eq0. - by rewrite gt_eqF. -move: (@cvg_expr _ z); rewrite (ltW z0) z1 => /(_ isT). -move/cvg_distP/(_ _ ea1z_gt0) => {ea1z_gt0} [k _ geo_k]. -rewrite near_map; near=> n. -have [m nkm] : exists m, n = ((k + m).+1)%nat. - have nk : (k < n)%nat by near: n; exists k.+1. - exists (n - k.+1)%nat. - rewrite subnS -subn1 addnBA ?subn_gt0 // addnBA; last exact/ltnW. - by rewrite -addnBAC // subnn add0n subn1 prednK // (leq_trans _ nk). -rewrite nkm -/(series _ _) geometric_seriesE; last by rewrite lt_eqF. -rewrite -{1}(mulr1 a) -mulrBl -mulrBr opprB addrCA subrr addr0. -rewrite mulrAC normrM (mulrC `|_ / _|) -ltr_pdivl_mulr; last first. - by rewrite normr_gt0 mulf_eq0 negb_or a0 /= invr_eq0 subr_eq0 gt_eqF. -by rewrite -nkm -normrN -sub0r geo_k // nkm -addnS leq_addr. -Grab Existential Variables. all: end_near. Qed. +Lemma cvg_geometric (R : archiFieldType) (a z : R) : `|z| < 1 -> + (geometric a z --> (0 : R^o)). +Proof. by move=> /cvg_geometric_series/cvgP/cvg_series_cvg_0. Qed. -Lemma is_cvg_geometric_series (R : archiFieldType) (a z : R) : - 0 < z < 1 -> cvg (series (geometric a z)). -Proof. by move=> z01; apply/cvg_ex; eexists; exact: cvg_geometric_series. Qed. +Lemma is_cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 -> + cvg (series (geometric a z)). +Proof. by move=> /cvg_geometric_series/cvgP; apply. Qed. Definition normed_series_of (K : numDomainType) (V : normedModType K) (u_ : V ^nat) of phantom V^nat (series u_) : K^o ^nat := @@ -844,7 +821,7 @@ have [Spoo|Spoo] := pselect (S +oo%E). case: Spoo => N _ uNoo; exists N => n Nn. by move: (nd_u_ _ _ Nn); rewrite uNoo lee_pinfty_eq => /eqP. have -> : l = +oo%E by rewrite /l /ereal_sup; exact: supremum_pinfty. - rewrite -(cvg_comp_addn N); set f := (X in X --> _). + rewrite -(cvg_shiftn N); set f := (X in X --> _). rewrite (_ : f = (fun=> +oo%E)); first exact: cvg_cst. by rewrite funeqE => n; rewrite /f /= Nu // leq_addl. have [Snoo|Snoo] := pselect (u_ = fun=> -oo%E).