diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6d3bc729b0..d90a8985a4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -25,11 +25,16 @@ from level 36 to 34 and level of `F` from 36 to 41. In particular, this means that `\int[mu]_(x in D) f x * g x` now parses as `\int[mu]_(x in D) (f x * g x)`. +- in `sequences.v`, + + lemmas `is_cvg_series_shiftn`, `near_series_squeeze_is_cvgn` + +### Changed ### Renamed - in `sequences.v`: + `limn_einf_shift` -> `limn_einf_addl` + + `series_le_cvg` -> `series_squeeze_is_cvgn` ### Generalized diff --git a/theories/elementary_functions/trigonometry_functions.v b/theories/elementary_functions/trigonometry_functions.v index 5369a0ba33..2f2a410d52 100644 --- a/theories/elementary_functions/trigonometry_functions.v +++ b/theories/elementary_functions/trigonometry_functions.v @@ -59,7 +59,6 @@ From mathcomp Require Import landau sequences derive realfun exp realfun. (* *) (******************************************************************************) -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -156,7 +155,7 @@ Proof. by rewrite /sin_coeff /= odd_double /= !mul0r. Qed. Lemma is_cvg_series_sin_coeff x : cvg (series (sin_coeff x) @ \oo). Proof. apply: normed_cvg. -apply: series_le_cvg; last exact: (is_cvg_series_exp_coeff `|x|). +apply: series_squeeze_is_cvgn; last exact: (is_cvg_series_exp_coeff `|x|). - by move=> n; rewrite normr_ge0. - by move=> n; rewrite divr_ge0. - move=> n /=; rewrite /exp_coeff /sin_coeff /=. @@ -234,7 +233,7 @@ Qed. Lemma is_cvg_series_cos_coeff x : cvg (series (cos_coeff x) @ \oo). Proof. apply: normed_cvg. -apply: series_le_cvg; last exact: (is_cvg_series_exp_coeff `|x|). +apply: series_squeeze_is_cvgn; last exact: (is_cvg_series_exp_coeff `|x|). - by move=> n; rewrite normr_ge0. - by move=> n; rewrite divr_ge0. - move=> n /=; rewrite /exp_coeff /cos_coeff /=. diff --git a/theories/exp.v b/theories/exp.v index 4131b8837d..bb4aca72ea 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -66,7 +66,7 @@ Proof. move=> Cx zLx; have [K [Kreal Kf]] := cvg_series_bounded Cx. have Kzxn n : 0 <= `|K + 1| * `|z ^+ n| / `|x ^+ n| by rewrite !mulr_ge0. apply: normed_cvg. -apply: series_le_cvg Kzxn _ _ => [//=| /= n|]. +apply: series_squeeze_is_cvgn Kzxn _ _ => [//=| /= n|]. rewrite (_ : `|_ * _| = `|f n * x ^+ n| * `|z ^+ n| / `|x ^+ n|). rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC. by case: ltrgt0P zLx; rewrite //= normr_lt0. @@ -1470,7 +1470,7 @@ have : forall n, harmonic n <= riemannR a n. move=> [/=|n]; first by rewrite powR1 invr1. rewrite -[leRHS]div1r ler_pdivlMr ?powR_gt0// mulrC ler_pdivrMr//. by rewrite mul1r -[leRHS]powRr1// ler_powR// ler1n. -move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). +move/(series_squeeze_is_cvgn harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). by move/contra_not; apply; exact: dvg_harmonic. Qed. diff --git a/theories/numfun.v b/theories/numfun.v index c29703ca18..3ffff640df 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1407,7 +1407,8 @@ exists (lim (h_ @ \oo)); split. rewrite -fmap_comp /comp /h_ => <-. under [fun _ : nat => _]eq_fun => ? do rewrite /series /= fct_sumE. have cvg_gt : cvgn [normed series (g_^~ t)]. - apply: (series_le_cvg _ _ (g_bd ^~ t) (is_cvg_geometric_series _)) => //. + apply: (series_squeeze_is_cvgn _ _ (g_bd ^~ t) + (is_cvg_geometric_series _)) => //. by move=> n; rewrite mulr_ge0. rewrite (le_trans (lim_series_norm _))//; apply: le_trans. exact/(lim_series_le cvg_gt _ (g_bd ^~ t))/is_cvg_geometric_series. diff --git a/theories/sequences.v b/theories/sequences.v index da56eb1f40..f8cf695e84 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -558,7 +558,7 @@ Proof. by rewrite telescopeK/= addrC addrNK. Qed. Section series_patched. Context (N : nat) {K : numFieldType} {V : normedModType K}. -Implicit Types (f : nat -> V) (u : V ^nat) (l : set_system V). +Implicit Types (f : nat -> V) (u : V ^nat) (l : set_system V). Lemma is_cvg_series_restrict u_ : cvgn [sequence \sum_(N <= k < n) u_ k]_n = cvgn (series u_). @@ -571,6 +571,20 @@ rewrite funeqE => n; case: leqP => // ltNn; apply: (canRL (addrK _)). by rewrite seriesEnat addrC -big_cat_nat// ltnW. Qed. +Lemma is_cvg_series_shiftn u_ : cvgn (series u_) <-> cvgn [series u_ (n + N)]_n. +Proof. +split. +- rewrite -is_cvg_series_restrict => /cvg_ex[/= l +]. + rewrite -(cvg_shiftn N)/= => Nnul; apply: cvgP; apply: cvg_trans Nnul. + apply: near_eq_cvg; near=> n. + rewrite /series/=. + by rewrite -{1}(add0n N) big_addn addnK. +- move=> cvgu; rewrite -is_cvg_series_restrict. + apply: cvgP; rewrite -(cvg_shiftn N)/=; apply: cvg_trans cvgu. + apply: near_eq_cvg; near=> n => /=. + by rewrite -{2}(add0n N) big_addn addnK. +Unshelve. all: by end_near. Qed. + End series_patched. Section sequences_R_lemmas. @@ -972,7 +986,7 @@ have := su_cv; rewrite near_swap => su_cvC; near=> m => /=; rewrite sub_series. by have [|/ltnW]:= leqP m.2 m.1 => m12; rewrite ?normrN; near: m. Unshelve. all: by end_near. Qed. -Lemma series_le_cvg (R : realType) (u_ v_ : R ^nat) : +Lemma series_squeeze_is_cvgn {R : realType} (u_ v_ : R ^nat) : (forall n, 0 <= u_ n) -> (forall n, 0 <= v_ n) -> (forall n, u_ n <= v_ n) -> cvgn (series v_) -> cvgn (series u_). @@ -980,8 +994,29 @@ Proof. move=> u_ge0 v_ge0 le_uv /cvg_seq_bounded/bounded_fun_has_ubound[M v_M]. apply: nondecreasing_is_cvgn; first exact: nondecreasing_series. exists M => _ [n _ <-]. -by apply: le_trans (v_M (series v_ n) _); [apply: ler_sum | exists n]. +by apply: le_trans (v_M (series v_ n) _); [exact: ler_sum | exists n]. Qed. +#[deprecated(since="mathcomp-analysis 1.19.0", use=series_squeeze_is_cvgn)] +Notation series_le_cvg := series_squeeze_is_cvgn (only parsing). + +Lemma near_series_squeeze_is_cvgn {R : realType} (u_ v_ : R^nat) : + (\forall n \near \oo, 0 <= u_ n) -> (\forall n \near \oo, 0 <= v_ n) -> + (\forall n \near \oo, u_ n <= v_ n) -> + cvgn (series v_) -> cvgn (series u_). +Proof. +move=> u0 v0 uv cvg_v. +near \oo => N; apply/(is_cvg_series_shiftn N). +move: cvg_v => /(is_cvg_series_shiftn N); apply: series_le_cvg => /= n. +- have : forall n, (n >= N)%N -> 0 <= u_ n. + by near: N; exact: (iffLR (near_infty_leq _)). + by apply; exact: leq_addl. +- have : forall n, (n >= N)%N -> 0 <= v_ n. + by near: N; exact: (iffLR (near_infty_leq _)). + by apply; exact: leq_addl. +- have : forall n, (n >= N)%N -> u_ n <= v_ n. + by near: N; exact: (iffLR (near_infty_leq _)). + by apply; exact: leq_addl. +Unshelve. all: by end_near. Qed. Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) : cvgn [normed series u_] -> cvgn (series u_). @@ -1039,19 +1074,18 @@ move=> k_gt0 Cf Hg. apply: (@cvg_to_0_linear _ _ (limn (series f)) k) => // h hLk; rewrite mulrC. have Ckf : cvgn (series (`|h| *: f)) := @is_cvg_seriesZ _ _ `|h| Cf. have Cng : cvgn [normed series (g h)]. - apply: series_le_cvg (Hg _ hLk) _ => [//|?|]. + apply: series_squeeze_is_cvgn (Hg _ hLk) _ => [//|?|]. exact: le_trans (Hg _ hLk _). by under eq_fun do rewrite mulrC. apply: (le_trans (@lim_series_norm _ R^o _ Cng)). rewrite -[_ * _](lim_seriesZ _ Cf) (lim_series_le Cng Ckf) // => n. -by rewrite [leRHS]mulrC; apply: Hg. +by rewrite [leRHS]mulrC; exact: Hg. Qed. End series_linear. Section exponential_series. - -Variable R : realType. +Context {R : realType}. Implicit Types x : R. Definition exp_coeff x := [sequence x ^+ n / n`!%:R]_n.