From ca678fa4045f428fecc053c2bd191eb41449ea55 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 25 Mar 2025 18:46:56 +0900 Subject: [PATCH 1/2] exp_coeff_gt0 --- CHANGELOG_UNRELEASED.md | 3 +++ theories/sequences.v | 7 +++++++ 2 files changed, 10 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b4d0f0a4b..74588f173 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,6 +36,9 @@ - in `derive.v`: + lemmas `derive_shift`, `is_derive_shift` +- in `sequences.v`: + + lemma `exp_coeff_gt0` + ### Changed - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package diff --git a/theories/sequences.v b/theories/sequences.v index a94ac54f8..b071033e9 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1121,6 +1121,13 @@ Definition exp_coeff x := [sequence x ^+ n / n`!%:R]_n. Local Notation exp := exp_coeff. +Lemma exp_coeff_gt0 x n : 0 < x -> 0 < exp x n. +Proof. +move=> x0; rewrite /exp/= divr_gt0//. + by rewrite exprn_gt0. +by rewrite (_:0%R = 0%:R)// ltr_nat; exact: fact_gt0. +Qed. + Lemma exp_coeff_ge0 x n : 0 <= x -> 0 <= exp x n. Proof. by move=> x0; rewrite /exp divr_ge0 // exprn_ge0. Qed. From 94415b525b1eb8782fa3862bbcc5e3664d66d081 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 25 Mar 2025 19:24:36 +0900 Subject: [PATCH 2/2] exp_coeff_properties --- CHANGELOG_UNRELEASED.md | 5 +++ theories/exp.v | 68 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 74588f173..e42fe5f95 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -39,6 +39,11 @@ - in `sequences.v`: + lemma `exp_coeff_gt0` +- in `exp.v`: + + lemmas `normr_exp_coeff_near_nonincreasing`, + `series_exp_coeff_near_nondecreasing`, + `exp_coeff2_near_in_increasing` + ### Changed - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package diff --git a/theories/exp.v b/theories/exp.v index 803361b89..727dafc36 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -549,6 +549,74 @@ Local Close Scope convex_scope. End expR. +Section exp_coeff_properties. +Variable R : realType. +Implicit Types x : R. + +Lemma normr_exp_coeff_near_nonincreasing x : + \forall n \near \oo, + `|exp_coeff x n.+1| <= `|exp_coeff x n|. +Proof. +exists `|archimedean.Num.Def.ceil x |%N => //. +move=> n/= H. +rewrite exp_coeffE exprS mulrA normrM [leRHS]normrM ler_pM//. +rewrite factS mulnC natrM invfM -mulrA normrM ler_piMr//. +rewrite normrM normfV ler_pdivrMl; last by rewrite normr_gt0 lt0r_neq0. +by rewrite mulr1 (le_trans (abs_ceil_ge _))// gtr0_norm// ler_nat ltnS. +Qed. + +Lemma series_exp_coeff_near_ge0 x: + \forall n \near \oo, 0 <= (series (exp_coeff x)) n. +Proof. +apply: (cvgr_ge (expR x)); last exact: expR_gt0. +exact: is_cvg_series_exp_coeff. +Qed. + +Lemma exp_coeff2_near_nondecreasing x : + \forall N \near \oo, nondecreasing_seq + (fun n => (series (exp_coeff x) (2 * (n + N))%N)). +Proof. +have -[N _ Hnear] := normr_exp_coeff_near_nonincreasing x. +exists N => //n/= Nn; apply/nondecreasing_seqP => k. +rewrite /series/= addSn mulnS add2n !big_nat_recr//= -addrA lerDl. +rewrite -[X in _ <= _ + X]opprK subr_ge0 (le_trans (ler_norm _))// normrN. +have : (N <= (2 * (k + n)))%N. + by rewrite mulnDr -(add0n N) leq_add// mulSn mul1n -(add0n N) leq_add. +move/Hnear => H; rewrite (le_trans H)// ler_norml lexx andbT. +suff Hsuff : 0 <= exp_coeff x (2 * (k + n))%N. + by apply: (le_trans _ Hsuff); rewrite lerNl oppr0. +by rewrite mulr_ge0// exprn_even_ge0// mul2n odd_double. +Qed. + +Lemma exp_coeff2_near_in_increasing x : + \forall N \near \oo, {in [set k | (N <= k)%N] &, +nondecreasing_seq (fun n => (series (exp_coeff x) (2 * n)%N))}. +Proof. +have -[N _ Hnear] := normr_exp_coeff_near_nonincreasing x. +exists N => //k/= Nk n m; rewrite !inE/= => kn km nm. +have kn2 : (2 * k <= 2 * n)%N by rewrite leq_pmul2l. +have km2 : (2 * k <= 2 * m)%N by rewrite leq_pmul2l. +rewrite /series/= (big_cat_nat _ _ _ _ kn2)// (big_cat_nat _ _ _ _ km2)// lerD2. +have nm2 : (2 * n <= 2 * m)%N by rewrite leq_pmul2l. +rewrite (big_cat_nat _ _ _ _ nm2)//=. +rewrite lerDl -(add0n (2 * n)%N) big_addn -mulnBr. +elim: (m - n)%N; first by rewrite muln0 big_mkord big_ord0. +move=> {km nm km2 nm2} {}m IH. +rewrite mul2n doubleS 2?big_nat_recr//= -addrA addr_ge0// -?mul2n//. +rewrite -[X in _ <= _ + X]opprK subr_ge0 (le_trans (ler_norm _))// normrN. +rewrite addSn -mulnDr. +have : (N <= (2 * (m + n)))%N. + rewrite mulnDr -(add0n N) leq_add//. + by rewrite (leq_trans _ kn2)// (leq_trans Nk)// leq_pmull. +move/Hnear => H. +rewrite (le_trans H)// ler_norml lexx andbT. +suff Hsuff : 0 <= exp_coeff x (2 * (m + n))%N. + by rewrite (le_trans _ Hsuff)// lerNl oppr0. +by rewrite mulr_ge0// exprn_even_ge0// mul2n odd_double. +Qed. + +End exp_coeff_properties. + #[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRM_natl`")] Notation expRMm := expRM_natl (only parsing).