expR_ge1Dxn (math-comp#1638)

* expR_ge1Dxn

Author: IshiguroYoshihiro

CHANGELOG_UNRELEASED.md

@@ -66,6 +66,8 @@
   + definition `exponential_prob`
   + lemmas `derive1_exponential_pdf`, `exponential_prob_itv0c`,
     `integral_exponential_pdf`, `integrable_exponential_pdf`
+- in `exp.v`
+  + lemma `expR_ge1Dxn`
 
 ### Changed
 

theories/exp.v

@@ -170,9 +170,9 @@ rewrite -mulrA mulrC -mulrA mulr_natl -[X in _ *+ X]subn0 -sumr_const_nat.
 apply ler_sum_nat => i /=.
 case: n => //= n ni.
 rewrite normrM.
-pose d := (n.-1 - i)%nat.
-rewrite -[(n - i)%nat]prednK ?subn_gt0// predn_sub -/d.
-rewrite -(subnK (_ : i <= n.-1)%nat) -/d; last first.
+pose d := (n.-1 - i)%N.
+rewrite -[(n - i)%N]prednK ?subn_gt0// predn_sub -/d.
+rewrite -(subnK (_ : i <= n.-1)%N) -/d; last first.
   by rewrite -ltnS prednK// (leq_ltn_trans _ ni).
 rewrite addnC exprD mulrAC -mulrA.
 apply: ler_pM => //.
@@ -182,7 +182,7 @@ apply: le_trans (_ : d.+1%:R * K ^+ d <= _); last first.
   by rewrite ler_nat ltnS /d -subn1 -subnDA leq_subr.
 rewrite (le_trans (ler_norm_sum _ _ _))//.
 rewrite mulr_natl -[X in _ *+ X]subn0 -sumr_const_nat ler_sum_nat//= => j jd1.
-rewrite -[in leRHS](subnK (_ : j <= d)%nat) -1?ltnS // addnC exprD normrM.
+rewrite -[in leRHS](subnK (_ : j <= d)%N) -1?ltnS // addnC exprD normrM.
 by rewrite ler_pM// normrX lerXn2r// qualifE/= (le_trans _ zLK).
 Qed.
 
@@ -319,23 +319,33 @@ rewrite -addn1 series_addn series_exp_coeff0 big_add1 big1 ?addr0//.
 by move=> i _; rewrite /exp_coeff /= expr0n mul0r.
 Unshelve. all: by end_near. Qed.
 
-Local Lemma expR_ge1Dx_subproof x : 0 <= x -> 1 + x <= expR x.
+Lemma expR_ge1Dxn x n : 0 <= x -> 1 + x ^+ n.+1 / n.+1`!%:R <= expR x.
 Proof.
 move=> x_ge0; rewrite /expR.
-pose f (x : R) i := (i == 0%nat)%:R + x *+ (i == 1%nat).
-have F n : (1 < n)%nat -> \sum_(0 <= i < n) (f x i) = 1 + x.
-  move=> /subnK<-.
-  by rewrite addn2 !big_nat_recl //= /f /= mulr1n !mulr0n big1 ?add0r ?addr0.
-have -> : 1 + x = limn (series (f x)).
-  by apply/esym/lim_near_cst => //; near=> n; apply: F; near: n.
-apply: ler_lim; first by apply: is_cvg_near_cst; near=> n; apply: F; near: n.
+pose f n (x : R) i := (i == 0)%:R + x ^+ n / n`!%:R *+ (i == n).
+have F m : (n.+1 < m)%N ->
+    \sum_(0 <= i < m) (f n.+1 x i) = 1 + x ^+ n.+1 / n.+1`!%:R.
+  move=> n1m.
+  rewrite (@big_cat_nat _ _ _ n.+2)//= big_nat_recr// big_nat_recl//=.
+  rewrite big_nat_cond big1 ?addr0; last first.
+    by move=> i /[!andbT] /[!leq0n]/= ni; rewrite /f/= lt_eqF//= add0r.
+  rewrite big_nat_cond big1 ?addr0; last first.
+    move=> i /[!andbT] /andP[ni mi]; rewrite /f !gtn_eqF//= ?add0r//.
+    exact: ltn_trans ni.
+  by rewrite /f/= add0r mulr0n addr0 eqxx 2!mulr1n.
+rewrite [leLHS](_ : _ = limn (series (f n.+1 x))); last first.
+  by apply/esym/(@lim_near_cst R^o) => //; near=> k; apply: F; near: k.
+apply: ler_lim; first by apply: is_cvg_near_cst; near=> k; apply: F; near: k.
   exact: is_cvg_series_exp_coeff.
-by near=> n; apply: ler_sum => -[|[|i]] _;
-  rewrite /f /exp_coeff /= !(mulr0n, mulr1n, expr0, expr1, divr1, addr0, add0r)
-          // exp_coeff_ge0.
+near=> k; apply: ler_sum => -[|[|i]] _; rewrite /f /exp_coeff/= ?add0r.
+- by rewrite !(mulr0n, expr0, addr0, divr1).
+- case: n F; first by rewrite !(mulr0n, mulr1n, expr0, addr0, add0r, divr1).
+  by move=> n F; rewrite mulr0n expr1 divr1.
+- rewrite eqSS; case: eqP => [->|_]; rewrite ?mulr1n//.
+  by rewrite mulr0n divr_ge0// exprn_ge0.
 Unshelve. all: by end_near. Qed.
 
-Lemma exp_coeffE x : exp_coeff x = (fun n => (fun n => (n`!%:R)^-1) n * x ^+ n).
+Lemma exp_coeffE x : exp_coeff x = fun n => (fun n => (n`!%:R)^-1) n * x ^+ n.
 Proof. by apply/funext => i; rewrite /exp_coeff /= mulrC. Qed.
 
 Import GRing.Theory.
@@ -386,7 +396,8 @@ Proof. by rewrite -[X in _ X * _ = _]addr0 expRxDyMexpx expR0. Qed.
 
 Lemma pexpR_gt1 x : 0 < x -> 1 < expR x.
 Proof.
-by move=> x0; rewrite (lt_le_trans _ (expR_ge1Dx_subproof (ltW x0)))// ltrDl.
+move=> x0; rewrite (lt_le_trans _ (expR_ge1Dxn 0%N (ltW x0)))// ltrDl.
+by rewrite expr1 divr1.
 Qed.
 
 Lemma expR_gt0 x : 0 < expR x.