diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5e316b600..269dedc6d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/theories/sequences.v b/theories/sequences.v index 443235f73..da8930353 100644 --- a/theories/sequences.v +++ b/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_ F i == lim (fun n => (\sum_) F i)) where can *) (* be (i 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 (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope. Notation "\big [ op / idx ]_ ( m <= i //; 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.