Merge pull request #380 from math-comp/exponential_series

Exponential series

CHANGELOG_UNRELEASED.md

@@ -81,6 +81,12 @@
   + notation `0`/`1` for `0%R%:E`/`1%R:%E` in `ereal_scope`
 - file `reals.v`:
   + lemmas `le_floor`, `le_ceil`
+- in `sequences,v`:
+  + lemmas `leq_fact`, `prod_rev`, `fact_split`
+  + definition `exp_coeff`
+  + lemmas `exp_coeff_ge0`, `series_exp_coeff0`, `is_cvg_series_exp_coeff_pos`,
+    ` normed_series_exp_coeff`, `is_cvg_series_exp_coeff `, `cvg_exp_coeff`
+  + definition `expR`
 
 ### Changed
 

theories/sequences.v

@@ -8,9 +8,10 @@ Require Import classical_sets posnum topology normedtype landau.
 (*                Definitions and lemmas about sequences                      *)
 (*                                                                            *)
 (* The purpose of this file is to gather generic definitions and lemmas about *)
-(* sequences. Since it is an early version, it is likely to undergo changes.  *)
-(* Here follow sample definitions and lemmas to give an idea of contents.     *)
-(* See file sequences_applications.v for small scale usage examples.          *)
+(* sequences. The first part is essentially about sequences of realType       *)
+(* numbers while the last part is about extended real numbers. It is an early *)
+(* version that is likely to undergo changes. The documentation lists up      *)
+(* sample definitions and lemmas to give an idea of contents.                 *)
 (*                                                                            *)
 (* Definitions:                                                               *)
 (*           R ^nat == notation for sequences,                                *)
@@ -27,28 +28,31 @@ Require Import classical_sets posnum topology normedtype landau.
 (*                        cvg [norm S_n])                                     *)
 (*                                                                            *)
 (* Lemmas:                                                                    *)
-(*                       squeeze == squeeze lemma                             *)
-(*                 cvgNpinfty u_ == (- u_ --> +oo) = (u_ --> -oo).            *)
-(*    nonincreasing_cvg_ge u_ == if u_ is nonincreasing and convergent then   *)
-(*                                  forall n, lim u_ <= u_ n                  *)
-(*    nondecreasing_cvg_le u_ == if u_ is nondecreasing and convergent then   *)
-(*                                  forall n, lim u_ >= u_ n                  *)
-(*       nondecreasing_cvg u_ == if u_ is nondecreasing and bounded then u_   *)
-(*                                  is convergent and its limit is sup u_n    *)
-(*       nonincreasing_cvg u_ == if u_ is nonincreasing u_ and bound by below *)
-(*                                  then u_ is convergent                     *)
-(*                      adjacent == adjacent sequences lemma                  *)
-(*                        cesaro == Cesaro's lemma                            *)
+(*                  squeeze == squeeze lemma                                  *)
+(*            cvgNpinfty u_ == (- u_ --> +oo) = (u_ --> -oo).                 *)
+(*  nonincreasing_cvg_ge u_ == if u_ is nonincreasing and convergent then     *)
+(*                             forall n, lim u_ <= u_ n                       *)
+(*  nondecreasing_cvg_le u_ == if u_ is nondecreasing and convergent then     *)
+(*                             forall n, lim u_ >= u_ n                       *)
+(*     nondecreasing_cvg u_ == if u_ is nondecreasing and bounded then u_     *)
+(*                             is convergent and its limit is sup u_n         *)
+(*     nonincreasing_cvg u_ == if u_ is nonincreasing u_ and bound by below   *)
+(*                             then u_ is convergent                          *)
+(*                 adjacent == adjacent sequences lemma                       *)
+(*                   cesaro == Cesaro's lemma                                 *)
 (*                                                                            *)
-(* Sections sequences_R_* contain properties of sequences of real numbers     *)
+(* Sections sequences_R_* contain properties of sequences of real numbers.    *)
 (*                                                                            *)
-(* Section sequences_of_extended_real_numbers contain properties of sequences *)
-(* of extended real numbers.                                                  *)
+(* is_cvg_series_exp_coeff == convergence of \sum_n^+oo x^n / n!              *)
+(*                  expR x == the exponential function defined on a realType  *)
 (*                                                                            *)
 (* \sum_<range> F i == lim (fun n => (\sum_<range>) F i)) where <range> can   *)
 (*                     be (i <oo), (i <oo | P i), (m <= i <oo), or            *)
 (*                     (m <= i <oo | P i)                                     *)
 (*                                                                            *)
+(* Section sequences_ereal contain properties of sequences of extended real   *)
+(* numbers.                                                                   *)
+(*                                                                            *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -792,6 +796,149 @@ apply: filterS => n /=; rewrite ger0_norm ?sumr_ge0//.
 by apply: le_lt_trans; apply: ler_norm_sum.
 Qed.
 
+(* TODO: backport to MathComp? *)
+Section fact_facts.
+
+Local Open Scope nat_scope.
+
+Lemma leq_fact n : n <= n`!.
+Proof.
+by case: n => // n;  rewrite dvdn_leq ?fact_gt0 // dvdn_fact ?andTb.
+Qed.
+
+Lemma prod_rev n m :
+  \prod_(0 <= k < n - m) (n - k) = \prod_(m.+1 <= k < n.+1) k.
+Proof.
+rewrite [in RHS]big_nat_rev /= -{1}(add0n m.+1) big_addn subSS.
+by apply eq_bigr => i _; rewrite addnS subSS addnC subnDr.
+Qed.
+
+Lemma fact_split n m : m <= n -> n`! = \prod_(0 <= k < n - m) (n - k) * m`!.
+Proof.
+move=> ?; rewrite [in RHS]fact_prod mulnC prod_rev -big_cat [in RHS]/index_iota.
+rewrite subn1 -iota_add subSS addnBCA // subnn addn0 [in LHS]fact_prod.
+by rewrite [in RHS](_ : n = n.+1 - 1) // subn1.
+Qed.
+
+End fact_facts.
+
+Section exponential_series.
+
+Variable R : realType.
+Implicit Types x : R.
+
+Definition exp_coeff x := [sequence x ^+ n / n`!%:R]_n.
+
+Local Notation exp := exp_coeff.
+
+Lemma exp_coeff_ge0 x n : 0 <= x -> 0 <= exp x n.
+Proof. by move=> x0; rewrite /exp divr_ge0 // ?exprn_ge0 // ler0n. Qed.
+
+Lemma series_exp_coeff0 n : series (exp 0) n.+1 = 1.
+Proof.
+rewrite /series /= big_mkord big_ord_recl /= /exp /= expr0n divr1.
+by rewrite big1 ?addr0 // => i _; rewrite expr0n mul0r.
+Qed.
+
+Section exponential_series_cvg.
+
+Variable x : R.
+Hypothesis x0 : 0 < x.
+
+Let S0 N n := (N ^ N)%:R * \sum_(N.+1 <= i < n) (x / N%:R) ^+ i.
+
+Let is_cvg_S0 N : x < N%:R -> cvg (S0 N).
+Proof.
+move=> xN; apply: is_cvgZr; rewrite is_cvg_series_restrict exprn_geometric.
+apply/is_cvg_geometric_series; rewrite normrM normfV.
+by rewrite ltr_pdivr_mulr ?mul1r !ger0_norm // 1?ltW // (lt_trans x0).
+Qed.
+
+Let S0_ge0 N n : 0 <= S0 N n.
+Proof.
+rewrite mulr_ge0 // ?ler0n //; apply sumr_ge0 => i _.
+by rewrite exprn_ge0 // divr_ge0 // ?ler0n // ltW.
+Qed.
+
+Let S0_sup N n : x < N%:R -> S0 N n <= sup [set of S0 N].
+Proof.
+move=> xN; apply/sup_upper_bound; [split; [by exists (S0 N n), n|]|by exists n].
+rewrite (_ : [set of _] = [set `|S0 N n0| | n0 in setT]).
+  by apply: cvg_has_ub (is_cvg_S0 xN).
+by rewrite predeqE=> y; split=> -[z _ <-]; exists z; rewrite ?ger0_norm ?S0_ge0.
+Qed.
+
+Let S1 N n := \sum_(N.+1 <= i < n) exp x i.
+
+Lemma incr_S1 N : nondecreasing_seq (S1 N).
+Proof.
+apply/nondecreasing_seqP => n; rewrite /S1.
+have [nN|Nn] := leqP n N; first by rewrite !big_geq // (leq_trans nN).
+by rewrite big_nat_recr//= ler_addl exp_coeff_ge0 // ltW.
+Qed.
+
+Let S1_sup N n : x < N%:R -> S1 N n <= sup [set of S0 N].
+Proof.
+move=> xN; rewrite (le_trans _ (S0_sup n xN)) // /S0 big_distrr /=.
+have N_gt0 := lt_trans x0 xN.
+apply ler_sum => i _.
+have [Ni|iN] := ltnP N i; last first.
+  rewrite expr_div_n mulrCA ler_pmul2l ?exprn_gt0 // (@le_trans _ _ 1) //.
+    by rewrite invf_le1 ?ler1n ?ltr0n // fact_gt0.
+  rewrite natrX -expfB_cond ?(negPf (lt0r_neq0 N_gt0)) //.
+  by rewrite exprn_ege1 // ler1n; case: (N) xN x0; case: ltrgt0P.
+rewrite /exp expr_div_n /= (fact_split Ni) mulrCA.
+rewrite ler_pmul2l ?exprn_gt0 // natrX -invf_div -expfB //.
+rewrite lef_pinv ?qualifE; last 2 first.
+- rewrite ltr0n muln_gt0 fact_gt0 andbT.
+  rewrite big_mkord prodn_gt0  // => j.
+  by rewrite subn_gt0 (leq_trans (ltn_ord _) (leq_subr _ _)).
+- by rewrite exprn_gt0.
+rewrite prod_rev -natrX ler_nat -prod_nat_const_nat big_add1 /= big_ltn //.
+rewrite mulnC leq_mul //; last by apply: leq_trans (leq_fact _).
+rewrite -(subnK Ni); elim: (_ - _)%N => [|k IH]; first by rewrite !big_geq.
+rewrite !addSn !big_nat_recr //= ?leq_mul ?leq_addl //.
+by rewrite -addSn -addSnnS leq_addl.
+Qed.
+
+Lemma is_cvg_series_exp_coeff_pos : cvg (series (exp x)).
+Proof.
+rewrite /series; near \oo => N; have xN : x < N%:R; last first.
+  rewrite -(@is_cvg_series_restrict N.+1).
+  exact: (nondecreasing_is_cvg (incr_S1 N) (fun n => S1_sup n xN)).
+near: N; exists (absz (floor x)).+1 => // m; rewrite /mkset -(@ler_nat R).
+move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_Rfloor x)) // -addn1.
+rewrite natrD (_ : 1%:R = 1%R) // ler_add2r RfloorE -(@gez0_abs (floor x)) //.
+by rewrite floor_ge0// ltW.
+Grab Existential Variables. all: end_near. Qed.
+
+End exponential_series_cvg.
+
+Lemma normed_series_exp_coeff x : [normed series (exp x)] = series (exp `|x|).
+Proof.
+rewrite funeqE => n /=; apply: eq_bigr => k _.
+by rewrite /exp normrM normfV normrX [`|_%:R|]@ger0_norm.
+Qed.
+
+Lemma is_cvg_series_exp_coeff x : cvg (series (exp x)).
+Proof.
+have [/eqP ->|x0] := boolP (x == 0).
+  apply/cvg_ex; exists 1; apply/cvg_distP => // => _/posnumP[e].
+  rewrite near_map; near=> n; have [m ->] : exists m, n = m.+1.
+    by exists n.-1; rewrite prednK //; near: n; exists 1%N.
+  by rewrite series_exp_coeff0 subrr normr0.
+apply: normed_cvg; rewrite normed_series_exp_coeff.
+by apply: is_cvg_series_exp_coeff_pos; rewrite normr_gt0.
+Grab Existential Variables. all: end_near. Qed.
+
+Lemma cvg_exp_coeff x : exp x --> (0 : R).
+Proof. exact: (cvg_series_cvg_0 (@is_cvg_series_exp_coeff x)). Qed.
+
+End exponential_series.
+
+(* TODO: generalize *)
+Definition expR (R : realType) (x : R) : R := lim (series (exp_coeff x)).
+
 Notation "\big [ op / idx ]_ ( m <= i <oo | P ) F" :=
   (lim (fun n => (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope.
 Notation "\big [ op / idx ]_ ( m <= i <oo ) F" :=
@@ -810,7 +957,7 @@ Notation "\sum_ ( i <oo | P ) F" :=
 Notation "\sum_ ( i <oo ) F" :=
   (\big[+%E/0%:E]_(0 <= i <oo) F%E) : ring_scope.
 
-Section sequences_of_extended_real_numbers.
+Section sequences_ereal.
 Local Open Scope ereal_scope.
 
 Lemma ereal_cvgN (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) :
@@ -1297,4 +1444,4 @@ have : lim u <= M%:E by apply ereal_lim_le => //; near=> m; apply/ltW/Mu.
 by move/(lt_le_trans Ml); rewrite ltxx.
 Grab Existential Variables. all: end_near. Qed.
 
-End sequences_of_extended_real_numbers.
+End sequences_ereal.