From 82b5657192bf926aa114502f58247222df69a7e7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 May 2021 20:20:17 +0900 Subject: [PATCH 1/3] convergence of exponential series --- CHANGELOG_UNRELEASED.md | 5 ++ theories/sequences.v | 163 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 165 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5e316b600..9a696bfd4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,6 +81,11 @@ + 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` ### Changed diff --git a/theories/sequences.v b/theories/sequences.v index 443235f73..b847ca52a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -42,13 +42,15 @@ Require Import classical_sets posnum topology normedtype landau. (* *) (* Sections sequences_R_* contain properties of sequences of real numbers *) (* *) -(* Section sequences_of_extended_real_numbers contain properties of sequences *) -(* of extended real numbers. *) -(* *) (* \sum_ F i == lim (fun n => (\sum_) F i)) where can *) (* be (i // n ih; rewrite factS mulSn -(add1n n) leq_add // ?fact_gt0 //. +by rewrite leq_pmulr // fact_gt0. +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_nat_recl// /exp/= expr0n eqxx fact0 divr1 addrC. +by rewrite big1 ?add0r// => 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 ger0_norm ?(divr_ge0 (ltW _)) ?ler0n //. +by rewrite ltr_pdivr_mulr ?mul1r // (lt_trans _ xN). +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]). + exact: (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. +- rewrite (_ : index_iota _ _ = [::]) ?big_nil; last first. + by apply/eqP; rewrite -size_eq0 size_iota subn_eq0 (leq_trans nN). + rewrite (_ : index_iota _ _ = [::]) ?big_nil //. + by apply/eqP; rewrite -size_eq0 size_iota subSS subn_eq0 (leq_trans nN). +- by rewrite big_nat_recr//= ler_addl divr_ge0// ?ler0n// exprn_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 /=. +apply ler_sum => i _; have [Ni|iN] := ltnP N i; last first. + rewrite expr_div_n mulrCA ler_pmul2l ?exprn_gt0// (@le_trans _ _ 1) //. + rewrite invr_le1 ?ler1n ?ltr0n ?fact_gt0// unitfE pnatr_eq0 gtn_eqF//. + by rewrite fact_gt0. + rewrite natrX -exprB // ?unitfE; last by rewrite gt_eqF// (lt_trans _ xN). + move: iN; rewrite leq_eqVlt =>/orP[/eqP->|iN]; first by rewrite subnn expr0. + by rewrite exprn_ege1// ler1n (leq_trans _ iN). +rewrite /exp expr_div_n /= (fact_split Ni) mulrCA. +rewrite ler_pmul2l ?exprn_gt0 // natrX -invf_div -(exprB (ltnW Ni)); last first. + by rewrite unitfE gt_eqF // (lt_trans _ xN). +have ? : (0 < \prod_(0 <= k < i - N.+1) (i - k))%N. + rewrite big_seq_cond prodn_cond_gt0 //= => j. + rewrite andbT /index_iota mem_iota add0n leq0n /= subn0 => jiN. + by rewrite subn_gt0 (leq_trans jiN) //= leq_subr. +rewrite ler_pinv; last 2 first. + - rewrite inE unitfE natrM mulf_neq0 ?pnatr_eq0 -?lt0n ?fact_gt0 //= -natrM. + by rewrite ltr0n muln_gt0 fact_gt0 andbT. + - rewrite inE unitfE exprn_gt0// ?andbT ?(lt_trans _ xN)// gt_eqF//. + by rewrite exprn_gt0// (lt_trans _ xN). +rewrite (@le_trans _ _ + (\prod_(0 <= k < i - N.+1) (i - k) * N.+1 * N)%:R) //; last first. + by rewrite ler_nat -mulnA leq_mul2l factS leq_mul2l leq_fact 2!orbT. +rewrite -mulnA prod_rev mulnA mulnC (mulnC _ N.+1) !mulnA. +rewrite -(@prednK (i - N)) ?subn_gt0 // exprS !natrM -mulrA. +rewrite ler_pmul2l ?(lt_trans _ xN) //. +have [iN1|] := ltnP O (i - N).-1; last first. + rewrite leqn0 => /eqP->; rewrite expr0 -natrM ler1n muln_gt0 andTb. + by rewrite big_seq_cond prodn_cond_gt0// => -[|?]; rewrite mem_iota andbT. +rewrite -(@prednK (i - N).-1)// exprS ler_pmul// ?ler_nat ?exprn_ge0 ?ler0n//. +rewrite -subn1 /= subn_gt0 -addn1 ltn_subRL addn1 in iN1. +rewrite -natrX ler_nat -subn2 -subnDA addn2 -prod_nat_const_nat big_nat_recr//=. +rewrite -[X in (X <= _)%N]muln1 leq_mul// ?(leq_trans _ Ni)// -(@ler_nat R). +rewrite !natr_prod big_seq_cond [X in _ <= X]big_seq_cond; apply ler_prod=> j. +rewrite mem_iota andbT subnKC// => /andP[Nj ?]. +by rewrite ler0n ler_nat (leq_trans _ Nj)// (@leq_trans N.+1). +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. + Section sequences_of_extended_real_numbers. Local Open Scope ereal_scope. From 0b07491d0fe728cbc4305187e88a74d371e9c1bc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 25 May 2021 22:53:43 +0900 Subject: [PATCH 2/3] commit by Laurent Thery Co-Authored-By: thery --- theories/sequences.v | 78 ++++++++++++++++++-------------------------- 1 file changed, 31 insertions(+), 47 deletions(-) diff --git a/theories/sequences.v b/theories/sequences.v index b847ca52a..6d83db3d5 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -813,12 +813,12 @@ Notation "\sum_ ( i // n ih; rewrite factS mulSn -(add1n n) leq_add // ?fact_gt0 //. -by rewrite leq_pmulr // fact_gt0. +by case: n => // n; rewrite dvdn_leq ?fact_gt0 // dvdn_fact ?andTb. Qed. Lemma prod_rev n m : @@ -838,10 +838,12 @@ 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. @@ -849,11 +851,12 @@ 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_nat_recl// /exp/= expr0n eqxx fact0 divr1 addrC. -by rewrite big1 ?add0r// => i _; rewrite expr0n /= mul0r. +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. @@ -862,8 +865,8 @@ 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 ger0_norm ?(divr_ge0 (ltW _)) ?ler0n //. -by rewrite ltr_pdivr_mulr ?mul1r // (lt_trans _ xN). +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. @@ -876,7 +879,7 @@ 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]). - exact: (cvg_has_ub (is_cvg_S0 xN)). + by apply: cvg_has_ub (is_cvg_S0 xN). by rewrite predeqE=> y; split=> -[z _ <-]; exists z; rewrite ?ger0_norm ?S0_ge0. Qed. @@ -884,52 +887,33 @@ 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. -- rewrite (_ : index_iota _ _ = [::]) ?big_nil; last first. - by apply/eqP; rewrite -size_eq0 size_iota subn_eq0 (leq_trans nN). - rewrite (_ : index_iota _ _ = [::]) ?big_nil //. - by apply/eqP; rewrite -size_eq0 size_iota subSS subn_eq0 (leq_trans nN). -- by rewrite big_nat_recr//= ler_addl divr_ge0// ?ler0n// exprn_ge0// ltW. +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 /=. -apply ler_sum => i _; have [Ni|iN] := ltnP N i; last first. - rewrite expr_div_n mulrCA ler_pmul2l ?exprn_gt0// (@le_trans _ _ 1) //. - rewrite invr_le1 ?ler1n ?ltr0n ?fact_gt0// unitfE pnatr_eq0 gtn_eqF//. - by rewrite fact_gt0. - rewrite natrX -exprB // ?unitfE; last by rewrite gt_eqF// (lt_trans _ xN). - move: iN; rewrite leq_eqVlt =>/orP[/eqP->|iN]; first by rewrite subnn expr0. - by rewrite exprn_ege1// ler1n (leq_trans _ iN). +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 -(exprB (ltnW Ni)); last first. - by rewrite unitfE gt_eqF // (lt_trans _ xN). -have ? : (0 < \prod_(0 <= k < i - N.+1) (i - k))%N. - rewrite big_seq_cond prodn_cond_gt0 //= => j. - rewrite andbT /index_iota mem_iota add0n leq0n /= subn0 => jiN. - by rewrite subn_gt0 (leq_trans jiN) //= leq_subr. -rewrite ler_pinv; last 2 first. - - rewrite inE unitfE natrM mulf_neq0 ?pnatr_eq0 -?lt0n ?fact_gt0 //= -natrM. - by rewrite ltr0n muln_gt0 fact_gt0 andbT. - - rewrite inE unitfE exprn_gt0// ?andbT ?(lt_trans _ xN)// gt_eqF//. - by rewrite exprn_gt0// (lt_trans _ xN). -rewrite (@le_trans _ _ - (\prod_(0 <= k < i - N.+1) (i - k) * N.+1 * N)%:R) //; last first. - by rewrite ler_nat -mulnA leq_mul2l factS leq_mul2l leq_fact 2!orbT. -rewrite -mulnA prod_rev mulnA mulnC (mulnC _ N.+1) !mulnA. -rewrite -(@prednK (i - N)) ?subn_gt0 // exprS !natrM -mulrA. -rewrite ler_pmul2l ?(lt_trans _ xN) //. -have [iN1|] := ltnP O (i - N).-1; last first. - rewrite leqn0 => /eqP->; rewrite expr0 -natrM ler1n muln_gt0 andTb. - by rewrite big_seq_cond prodn_cond_gt0// => -[|?]; rewrite mem_iota andbT. -rewrite -(@prednK (i - N).-1)// exprS ler_pmul// ?ler_nat ?exprn_ge0 ?ler0n//. -rewrite -subn1 /= subn_gt0 -addn1 ltn_subRL addn1 in iN1. -rewrite -natrX ler_nat -subn2 -subnDA addn2 -prod_nat_const_nat big_nat_recr//=. -rewrite -[X in (X <= _)%N]muln1 leq_mul// ?(leq_trans _ Ni)// -(@ler_nat R). -rewrite !natr_prod big_seq_cond [X in _ <= X]big_seq_cond; apply ler_prod=> j. -rewrite mem_iota andbT subnKC// => /andP[Nj ?]. -by rewrite ler0n ler_nat (leq_trans _ Nj)// (@leq_trans N.+1). +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)). From a3943bc8d8e9d94f9c52bda57d0799e604ccf0cf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 30 May 2021 13:40:58 +0900 Subject: [PATCH 3/3] add `expR` definition and update documentation Co-Authored-By: thery --- CHANGELOG_UNRELEASED.md | 1 + theories/sequences.v | 86 ++++++++++++++++++++++------------------- 2 files changed, 47 insertions(+), 40 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9a696bfd4..269dedc6d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -86,6 +86,7 @@ + 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 6d83db3d5..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,29 +28,30 @@ 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. *) +(* *) +(* 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. -Notation "\big [ op / idx ]_ ( m <= i (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope. -Notation "\big [ op / idx ]_ ( m <= i (\big[ op / idx ]_(m <= i < n) F))) : big_scope. -Notation "\big [ op / idx ]_ ( i (\big[ op / idx ]_(i < n | P) F))) : big_scope. -Notation "\big [ op / idx ]_ ( i (\big[ op / idx ]_(i < n) F))) : big_scope. - -Notation "\sum_ ( m <= i (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope. +Notation "\big [ op / idx ]_ ( m <= i (\big[ op / idx ]_(m <= i < n) F))) : big_scope. +Notation "\big [ op / idx ]_ ( i (\big[ op / idx ]_(i < n | P) F))) : big_scope. +Notation "\big [ op / idx ]_ ( i (\big[ op / idx ]_(i < n) F))) : big_scope. + +Notation "\sum_ ( 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.