Library mathcomp.analysis.sequences

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
Require Import boolp reals ereal mathcomp_extra classical_sets signed functions.
Require Import topology normedtype landau.

Definitions and lemmas about sequences

The purpose of this file is to gather generic definitions and lemmas about sequences.

About sequences of real numbers:

[sequence u_n]_n == the sequence of general element u_n R ^nat == notation for the type of sequences, i.e., functions of type nat -> R seqDU F == sequence F_0, F_1 \ F_0, F_2 \ (F_0 U F_1),... seqD F == the sequence F_0, F_1 \ F_0, F_2 \ F_1,... series u == the sequence of partial sums of u telescope u := [sequence u n.+1 - u n]_n harmonic == harmonic sequence arithmetic == arithmetic sequence geometric == geometric sequence also arithmetic_mean, harmonic_mean, root_mean_square [series u_n]_n == the series of general element u_n [normed S] == transforms a series S = [series u_n]_n in its normed series [series `|u_n| ]_n] (useful to represent absolute and normed convergence: cvg [norm S_n]) exp_coeff n == the sequence of coefficients of the real exponential expR x == the exponential function defined on a realType is_cvg_series_exp_coeff == convergence of \sum_n^+oo x^n / n!

\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)

Sections sequences_R* contain properties of sequences of real numbers. For example: 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

About sequences of natural numbers:

nseries

About sequences of extended real numbers:

eseries, etelescope, etc.

Section sequences_ereal contain properties of sequences of extended real numbers.

Naming convention: lemmas about series of non-negative extended numbers use the string "nneseries" as part of their identifier

Limit superior and inferior:

sdrop u n := {u_k | k >= n} sups u := [sequence sup (sdrop u n) ]_n infs u := [sequence inf (sdrop u n) ]_n lim{inf,sup} == limit inferior/superior for realType esups u := [sequence ereal_sup (sdrop u n) ]_n einfs u := [sequence ereal_inf (sdrop u n) ]_n elim{inf,sup} == limit inferior/superior for \bar R

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "R ^nat" (at level 0).
Reserved Notation "a `^ x" (at level 11).
Reserved Notation "[ 'sequence' E ]_ n"
  (at level 0, E at level 200, n name, format "[ 'sequence' E ]_ n").
Reserved Notation "[ 'series' E ]_ n"
  (at level 0, E at level 0, n name, format "[ 'series' E ]_ n").
Reserved Notation "[ 'normed' E ]" (at level 0, format "[ 'normed' E ]").

Reserved Notation "\big [ op / idx ]_ ( m <= i <oo | P ) F"
  (at level 36, F at level 36, op, idx at level 10, m, i at level 50,
           format "'[' \big [ op / idx ]_ ( m <= i <oo | P ) F ']'").
Reserved Notation "\big [ op / idx ]_ ( m <= i <oo ) F"
  (at level 36, F at level 36, op, idx at level 10, i, m at level 50,
           format "'[' \big [ op / idx ]_ ( m <= i <oo ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i <oo | P ) F"
  (at level 36, F at level 36, op, idx at level 10, i at level 50,
           format "'[' \big [ op / idx ]_ ( i <oo | P ) '/ ' F ']'").
Reserved Notation "\big [ op / idx ]_ ( i <oo ) F"
  (at level 36, F at level 36, op, idx at level 10, i at level 50,
           format "'[' \big [ op / idx ]_ ( i <oo ) F ']'").

Reserved Notation "\sum_ ( m <= i '<oo' | P ) F"
  (at level 41, F at level 41, i, m at level 50,
           format "'[' \sum_ ( m <= i <oo | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( m <= i '<oo' ) F"
  (at level 41, F at level 41, i, m at level 50,
           format "'[' \sum_ ( m <= i <oo ) '/ ' F ']'").
Reserved Notation "\sum_ ( i '<oo' | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \sum_ ( i <oo | P ) '/ ' F ']'").
Reserved Notation "\sum_ ( i '<oo' ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \sum_ ( i <oo ) '/ ' F ']'").

Definition sequence R := nat → R.
Definition mk_sequence R f : sequence R := f.
Arguments mk_sequence R f /.
Notation "[ 'sequence' E ]_ n" := (mk_sequence (fun n ⇒ E%E)) : ereal_scope.
Notation "[ 'sequence' E ]_ n" := (mk_sequence (fun n ⇒ E)) : ring_scope.
Notation "R ^nat" := (sequence R) : type_scope.

Notation "'nondecreasing_seq' f" := ({homo f : n m / (n ≤ m)%nat >-> (n ≤ m)%O})
  (at level 10).
Notation "'nonincreasing_seq' f" := ({homo f : n m / (n ≤ m)%nat >-> (n ≥ m)%O})
  (at level 10).
Notation "'increasing_seq' f" := ({mono f : n m / (n ≤ m)%nat >-> (n ≤ m)%O})
  (at level 10).
Notation "'decreasing_seq' f" := ({mono f : n m / (n ≤ m)%nat >-> (n ≥ m)%O})
  (at level 10).

TODO: the "strict" versions with mono instead of homo should also have notations

Lemma nondecreasing_opp (T : numDomainType) (u_ : T ^nat) :
  nondecreasing_seq (- u_) = nonincreasing_seq u_.

Lemma nonincreasing_opp (T : numDomainType) (u_ : T ^nat) :
  nonincreasing_seq (- u_) = nondecreasing_seq u_.

Lemma decreasing_opp (T : numDomainType) (u_ : T ^nat) :
  decreasing_seq (- u_) = increasing_seq u_.

Lemma increasing_opp (T : numDomainType) (u_ : T ^nat) :
  increasing_seq (- u_) = decreasing_seq u_.

Lemma nondecreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) :
  (∀ n, u_ n ≤ u_ n.+1)%O ↔ nondecreasing_seq u_.

Lemma nonincreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) :
  (∀ n, u_ n ≥ u_ n.+1)%O ↔ nonincreasing_seq u_.

Lemma increasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) :
  (∀ n, u_ n < u_ n.+1)%O ↔ increasing_seq u_.

Lemma decreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) :
  (∀ n, u_ n > u_ n.+1)%O ↔ decreasing_seq u_.

TODO (maybe): variants for near \oo ??

Lemma lef_at (aT : Type) d (T : porderType d) (f : (aT → T )^nat) x :
  nondecreasing_seq f → {homo (f ^~ x ) : n m / (n ≤ m)%N >-> (n ≤ m)%O}.

Lemma nondecreasing_seqD T (d : unit) (R : numDomainType) (f g : (T → R )^nat) :
  (∀ x, nondecreasing_seq (f ^~ x )) →
  (∀ x, nondecreasing_seq (g ^~ x )) →
  (∀ x, nondecreasing_seq ((f \+ g ) ^~ x )).

Sequences of sets

Section seqDU.
Variables (T : Type).
Implicit Types F : (set T )^nat.

Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k.

Lemma trivIset_seqDU F : trivIset setT (seqDU F).

Lemma bigsetU_seqDU F n :
  \big[setU/set0]_(k < n) F k = \big[setU/set0]_(k < n) seqDU F k.

Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k.

End seqDU.
#[global] Hint Resolve trivIset_seqDU : core.

Section seqD.
Variable T : Type.
Implicit Types F : (set T ) ^nat.

Definition seqD F := fun n ⇒ if n isn't n'.+1 then F O else F n `\` F n'.

Lemma seqDUE F : nondecreasing_seq F → seqDU F = seqD F.

Lemma trivIset_seqD F : nondecreasing_seq F → trivIset setT (seqD F).

Lemma bigsetU_seqD F n :
  \big[setU/set0]_(i < n) F i = \big[setU/set0]_(i < n) seqD F i.

Lemma setU_seqD F : nondecreasing_seq F →
  ∀ n, F n.+1 = F n `|` seqD F n.+1.

Lemma eq_bigsetU_seqD F n : nondecreasing_seq F →
  F n = \big[setU/set0]_(i < n.+1) seqD F i.

Lemma eq_bigcup_seqD F : \bigcup_n F n = \bigcup_n seqD F n.

Lemma eq_bigcup_seqD_bigsetU F :
  \bigcup_n (seqD (fun n ⇒ \big[setU/set0]_(i < n.+1) F i) n ) = \bigcup_n F n.

End seqD.

Convergence of patched sequences

Section sequences_patched.

TODO: generalizations to numDomainType

Section NatShift.

Variables (N : nat) (V : topologicalType).
Implicit Types (f : nat → V) (u : V ^nat) (l : V).

Lemma cvg_restrict f u_ l :
  ([sequence if (n ≤ N)%N then f n else u_ n ]_n @ \oo --> l ) =
  (u_ @ \oo --> l ).

Lemma is_cvg_restrict f u_ :
  cvg ([sequence if (n ≤ N)%nat then f n else u_ n ]_n @ \oo) =
  cvg (u_ @ \oo).

Lemma cvg_centern u_ l : ([sequence u_ (n - N)%N]_n --> l ) = (u_ --> l ).

Lemma cvg_shiftn u_ l : ([sequence u_ (n + N)%N]_n --> l ) = (u_ --> l ).

End NatShift.

Variables (V : topologicalType).

Lemma cvg_shiftS u_ (l : V) : ([sequence u_ n.+1]_n --> l ) = (u_ --> l ).

End sequences_patched.

Section sequences_R_lemmas_realFieldType.
Variable R : realFieldType.
Implicit Types u v : R ^nat.

Lemma squeeze T (f g h : T → R) (a : filter_on T) :
  (\∀ x \near a , f x ≤ g x ≤ h x ) → ∀ (l : R),
  f @ a --> l → h @ a --> l → g @ a --> l.

Lemma cvgPpinfty (u_ : R ^nat) :
  u_ --> +oo ↔ ∀ A, \∀ n \near \oo , A ≤ u_ n.

Lemma cvgNpinfty u_ : (- u_ --> +oo ) = (u_ --> -oo ).

Lemma cvgNninfty u_ : (- u_ --> -oo ) = (u_ --> +oo ).

Lemma cvgPninfty (u_ : R ^nat) :
  u_ --> -oo ↔ ∀ A, \∀ n \near \oo , A ≥ u_ n.

Lemma ger_cvg_pinfty u_ v_ : (\∀ n \near \oo , u_ n ≤ v_ n ) →
  u_ --> +oo → v_ --> +oo.

Lemma ler_cvg_ninfty v_ u_ : (\∀ n \near \oo , u_ n ≤ v_ n ) →
  v_ --> -oo → u_ --> -oo.

Lemma lim_ge x u : cvg u → (\∀ n \near \oo , x ≤ u n ) → x ≤ lim u.

Lemma lim_le x u : cvg u → (\∀ n \near \oo , x ≥ u n ) → x ≥ lim u.

Lemma lt_lim u (M : R) : nondecreasing_seq u → cvg u → M < lim u →
  \∀ n \near \oo , M ≤ u n.

Lemma ler_lim u_ v_ : cvg u_ → cvg v_ →
  (\∀ n \near \oo , u_ n ≤ v_ n ) → lim u_ ≤ lim v_.

Lemma nonincreasing_cvg_ge u_ : nonincreasing_seq u_ → cvg u_ →
  ∀ n, lim u_ ≤ u_ n.

Lemma nondecreasing_cvg_le u_ : nondecreasing_seq u_ → cvg u_ →
  ∀ n, u_ n ≤ lim u_.

Lemma cvg_has_ub u_ : cvg u_ → has_ubound [set `|u_ n| | n in setT ].

Lemma cvg_has_sup u_ : cvg u_ → has_sup (u_ @` setT).

Lemma cvg_has_inf u_ : cvg u_ → has_inf (u_ @` setT).

End sequences_R_lemmas_realFieldType.

Section partial_sum.
Variables (V : zmodType) (u_ : V ^nat).

Definition series : V ^nat := [sequence \sum_(0 ≤ k < n) u_ k ]_n.
Definition telescope : V ^nat := [sequence u_ n.+1 - u_ n ]_n.

Lemma seriesEnat : series = [sequence \sum_(0 ≤ k < n) u_ k ]_n.

Lemma seriesEord : series = [sequence \sum_(k < n) u_ k ]_n.

Lemma seriesSr n : series n.+1 = series n + u_ n.

Lemma seriesS n : series n.+1 = u_ n + series n.

Lemma seriesSB (n : nat) : series n.+1 - series n = u_ n.

Lemma series_addn m n : series (n + m)%N = series m + \sum_(m ≤ k < n + m) u_ k.

Lemma sub_series_geq m n : (m ≤ n)%N →
  series n - series m = \sum_(m ≤ k < n) u_ k.

Lemma sub_series m n :
  series n - series m = if (m ≤ n)%N then \sum_(m ≤ k < n) u_ k
                        else - \sum_(n ≤ k < m) u_ k.

Lemma sub_double_series n : series n.*2 - series n = \sum_(n ≤ k < n.*2) u_ k.

End partial_sum.

Arguments series {V} u_ n : simpl never.
Arguments telescope {V} u_ n : simpl never.
Notation "[ 'series' E ]_ n" := (series [sequence E]_n) : ring_scope.

Lemma seriesN (V : zmodType) (f : V ^nat) : series (- f) = - series f.

Lemma seriesD (V : zmodType) (f g : V ^nat) : series (f + g) = series f + series g.

Lemma seriesZ (R : ringType) (V : lmodType R) (f : V ^nat) k :
  series (k *: f) = k *: series f.

Section partial_sum_numFieldType.
Variables V : numFieldType.
Implicit Types f g : V ^nat.

Lemma is_cvg_seriesN f : cvg (series (- f)) = cvg (series f).

Lemma lim_seriesN f : cvg (series f) → lim (series (- f)) = - lim (series f).

Lemma is_cvg_seriesZ f k : cvg (series f) → cvg (series (k *: f)).

Lemma lim_seriesZ f k : cvg (series f) →
  lim (series (k *: f)) = k *: lim (series f).

Lemma is_cvg_seriesD f g :
  cvg (series f) → cvg (series g) → cvg (series (f + g)).

Lemma lim_seriesD f g : cvg (series f) → cvg (series g) →
  lim (series (f + g)) = lim (series f) + lim (series g).

Lemma is_cvg_seriesB f g :
  cvg (series f) → cvg (series g) → cvg (series (f - g)).

Lemma lim_seriesB f g : cvg (series f) → cvg (series g) →
  lim (series (f - g)) = lim (series f) - lim (series g).

End partial_sum_numFieldType.

Lemma lim_series_le (V : realFieldType) (f g : V ^nat) :
  cvg (series f) → cvg (series g) → (∀ n, f n ≤ g n ) →
  lim (series f) ≤ lim (series g).

Lemma telescopeK (V : zmodType) (u_ : V ^nat) :
  series (telescope u_) = [sequence u_ n - u_ 0%N]_n.

Lemma seriesK (V : zmodType) : cancel (@series V) telescope.

Lemma eq_sum_telescope (V : zmodType) (u_ : V ^nat) n :
  u_ n = u_ 0%N + series (telescope u_) n.

Section series_patched.
Variables (N : nat) (K : numFieldType) (V : normedModType K).
Implicit Types (f : nat → V) (u : V ^nat) (l : V).

Lemma is_cvg_series_restrict u_ :
  cvg [sequence \sum_(N ≤ k < n) u_ k ]_n = cvg (series u_).

End series_patched.

Section sequences_R_lemmas.
Variable R : realType.

Lemma nondecreasing_cvg (u_ : R ^nat) :
    nondecreasing_seq u_ → has_ubound (range u_) →
  u_ --> sup (range u_).

Lemma nondecreasing_is_cvg (u_ : R ^nat) :
  nondecreasing_seq u_ → has_ubound (range u_) → cvg u_.

Lemma nondecreasing_dvg_lt (u_ : R ^nat) :
  nondecreasing_seq u_ → ¬ cvg u_ → u_ --> +oo.

Lemma near_nondecreasing_is_cvg (u_ : R ^nat) (M : R) :
    {near \oo , nondecreasing_seq u_} → (\∀ n \near \oo , u_ n ≤ M ) →
  cvg u_.

Lemma nonincreasing_cvg (u_ : R ^nat) :
    nonincreasing_seq u_ → has_lbound (range u_) →
  u_ --> inf (u_ @` setT).

Lemma nonincreasing_is_cvg (u_ : R ^nat) :
  nonincreasing_seq u_ → has_lbound (range u_) → cvg u_.

Lemma near_nonincreasing_is_cvg (u_ : R ^nat) (m : R) :
    {near \oo , nonincreasing_seq u_} → (\∀ n \near \oo , m ≤ u_ n ) →
  cvg u_.

Lemma adjacent (u_ v_ : R ^nat) : nondecreasing_seq u_ → nonincreasing_seq v_ →
  (v_ - u_) --> (0 : R ) → [/\ lim v_ = lim u_, cvg u_ & cvg v_].

End sequences_R_lemmas.

Definition harmonic {R : fieldType} : R ^nat := [sequence n.+1%:R^-1]_n.
Arguments harmonic {R} n /.

Lemma harmonic_gt0 {R : numFieldType} i : 0 < harmonic i :> R.

Lemma harmonic_ge0 {R : numFieldType} i : 0 ≤ harmonic i :> R.

Lemma cvg_harmonic {R : archiFieldType} : harmonic --> (0 : R ).

Lemma dvg_harmonic (R : numFieldType) : ¬ cvg (series (@harmonic R)).

Definition arithmetic_mean (R : numDomainType) (u_ : R ^nat) : R ^nat :=
  [sequence n.+1%:R^-1 × (series u_ n.+1)]_n.

Definition harmonic_mean (R : numDomainType) (u_ : R ^nat) : R ^nat :=
  let v := [sequence (u_ n)^-1]_n in
  [sequence (n.+1%:R / series v n.+1)]_n.

Definition root_mean_square (R : realType) (u_ : R ^nat) : R ^nat :=
  let v_ := [sequence (u_ k)^+2]_k in
  [sequence Num.sqrt (n.+1%:R^-1 × series v_ n.+1)]_n.

Section cesaro.
Variable R : archiFieldType.

Theorem cesaro (u_ : R ^nat) (l : R) : u_ --> l → arithmetic_mean u_ --> l.

End cesaro.

Section cesaro_converse.
Variable R : archiFieldType.

Let cesaro_converse_off_by_one (u_ : R ^nat) :
  [sequence n.+1%:R^-1 × series u_ n.+1]_ n --> (0 : R ) →
  [sequence n.+1%:R^-1 × series u_ n ]_ n --> (0 : R ).

Lemma cesaro_converse (u_ : R ^nat) (l : R) :
  telescope u_ =o_\oo harmonic → arithmetic_mean u_ --> l → u_ --> l.

End cesaro_converse.

Section series_convergence.

Lemma cvg_series_cvg_0 (K : numFieldType) (V : normedModType K) (u_ : V ^nat) :
  cvg (series u_) → u_ --> (0 : V ).

Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) :
  (∀ n, P n → 0 ≤ u_ n)%R →
  nondecreasing_seq (fun n⇒ \sum_(0 ≤ k < n | P k) u_ k)%R.

Lemma increasing_series (R : numFieldType) (u_ : R ^nat) :
  (∀ n, 0 < u_ n ) → increasing_seq (series u_).

End series_convergence.

Definition arithmetic (R : zmodType) a z : R ^nat := [sequence a + z *+ n ]_n.
Arguments arithmetic {R} a z n /.

Lemma mulrn_arithmetic (R : zmodType) : @GRing.natmul R = arithmetic 0.

Definition geometric (R : fieldType) a z : R ^nat := [sequence a × z ^+ n ]_n.
Arguments geometric {R} a z n /.

Lemma exprn_geometric (R : fieldType) : (@GRing.exp R ) = geometric 1.

Lemma cvg_arithmetic (R : archiFieldType) a (z : R) :
  z > 0 → arithmetic a z --> +oo.

Lemma cvg_expr (R : archiFieldType) (z : R) :
  `|z| < 1 → (GRing.exp z : R ^nat ) --> (0 : R ).

Lemma geometric_seriesE (R : numFieldType) (a z : R) : z != 1 →
  series (geometric a z) = [sequence a × (1 - z ^+ n) / (1 - z)]_n.

Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 →
  series (geometric a z) --> (a × (1 - z)^-1).

Lemma cvg_geometric_series_half (R : archiFieldType) (r : R) n :
  series (fun k ⇒ r / (2 ^ (k + n.+1))%:R : R^o) --> (r / 2 ^+ n : R^o).
Arguments cvg_geometric_series_half {R} _ _.

Lemma cvg_geometric (R : archiFieldType) (a z : R) : `|z| < 1 →
  geometric a z --> (0 : R ).

Lemma is_cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 →
cvg (series (geometric a z)).

Definition normed_series_of (K : numDomainType) (V : normedModType K)
    (u_ : V ^nat) of phantom V ^nat (series u_) : K ^nat :=
  [series `|u_ n|]_n.
Notation "[ 'normed' s_ ]" := (@normed_series_of _ _ _ (Phantom _ s_)) : ring_scope.
Arguments normed_series_of {K V} u_ _ n /.

Lemma ger0_normed {K : numFieldType} (u_ : K ^nat) :
  (∀ n, 0 ≤ u_ n ) → [normed series u_] = series u_.

Lemma cauchy_seriesP {R : numFieldType} (V : normedModType R) (u_ : V ^nat) :
  cauchy (series u_ @ \oo) ↔
  ∀ e : R, e > 0 →
    \∀ n \near (\oo , \oo ), `|\sum_(n .1 ≤ k < n .2) u_ k| < e.

Lemma series_le_cvg (R : realType) (u_ v_ : R ^nat) :
  (∀ n, 0 ≤ u_ n ) → (∀ n, 0 ≤ v_ n ) →
  (∀ n, u_ n ≤ v_ n ) →
  cvg (series v_) → cvg (series u_).

Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) :
  cvg [normed series u_] → cvg (series u_).

Lemma lim_series_norm {R : realType} (V : completeNormedModType R) (f : V ^nat) :
  cvg [normed series f ] → `|lim (series f)| ≤ lim [normed series f ].

Section series_linear.

Lemma cvg_series_bounded (R : realFieldType) (f : R ^nat) :
  cvg (series f) → bounded_fun f.

Lemma cvg_to_0_linear (R : realFieldType) (f : R → R) K k :
  0 < k → (∀ r, 0 < `| r | < k → `|f r| ≤ K × `| r |) →
    f x @[x --> 0^'] --> 0.

Lemma lim_cvg_to_0_linear (R : realType) (f : nat → R) (g : R → nat → R) k :
  0 < k → cvg (series f) →
  (∀ r, 0 < `|r| < k → ∀ n, `|g r n| ≤ f n × `| r |) →
  lim (series (g x)) @[x --> 0^'] --> 0.

End series_linear.

Section exponential_series.

Variable R : realType.
Implicit Types x : R.

Definition exp_coeff x := [sequence x ^+ n / n`!%:R]_n.

Lemma exp_coeff_ge0 x n : 0 ≤ x → 0 ≤ exp x n.

Lemma series_exp_coeff0 n : series (exp 0) n.+1 = 1.

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).

Let S0_ge0 N n : 0 ≤ S0 N n.

Let S0_sup N n : x < N%:R → S0 N n ≤ sup (range (S0 N)).

Let S1 N n := \sum_(N.+1 ≤ i < n) exp x i.

Lemma incr_S1 N : nondecreasing_seq (S1 N ).

Let S1_sup N : x < N%:R → ubound (range (S1 N)) (sup (range (S0 N))).

Lemma is_cvg_series_exp_coeff_pos : cvg (series (exp x)).

End exponential_series_cvg.

Lemma normed_series_exp_coeff x : [normed series (exp x)] = series (exp `|x|).

Lemma is_cvg_series_exp_coeff x : cvg (series (exp x)).

Lemma cvg_exp_coeff x : exp x --> (0 : R ).

End exponential_series.

Definition expR {R : realType} (x : R) : R := lim (series (exp_coeff x)).

Lemma nat_dvg_real (R : realType) (u_ : nat ^nat) : u_ --> \oo →
  ([sequence (u_ n)%:R : R^o]_n --> +oo)%R.

Lemma nat_cvgPpinfty (u : nat ^nat) :
  u --> \oo ↔ ∀ A, \∀ n \near \oo , (A ≤ u n)%N.

Lemma nat_nondecreasing_is_cvg (u_ : nat ^nat) :
  nondecreasing_seq u_ → has_ubound (range u_) → cvg u_.

Definition nseries (u : nat ^nat) := (fun n ⇒ \sum_(0 ≤ k < n) u k)%N.

Lemma le_nseries (u : nat ^nat) : {homo nseries u : a b / a ≤ b }%N.

Lemma cvg_nseries_near (u : nat ^nat) : cvg (nseries u) →
  \∀ n \near \oo , u n = 0%N.

Lemma dvg_nseries (u : nat ^nat) : ¬ cvg (nseries u) → nseries u --> \oo.

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" :=
  (lim (fun n ⇒ (\big[ op / idx ]_(m ≤ i < n) F))) : big_scope.
Notation "\big [ op / idx ]_ ( i <oo | P ) F" :=
  (lim (fun n ⇒ (\big[ op / idx ]_(i < n | P) F))) : big_scope.
Notation "\big [ op / idx ]_ ( i <oo ) F" :=
  (lim (fun n ⇒ (\big[ op / idx ]_(i < n) F))) : big_scope.

Notation "\sum_ ( m <= i <oo | P ) F" :=
  (\big [+%E /0%E]_(m ≤ i <oo | P%B) F%E) : ereal_scope.
Notation "\sum_ ( m <= i <oo ) F" :=
  (\big [+%E /0%E]_(m ≤ i <oo ) F%E) : ereal_scope.
Notation "\sum_ ( i <oo | P ) F" :=
  (\big [+%E /0%E]_(0 ≤ i <oo | P%B) F%E) : ereal_scope.
Notation "\sum_ ( i <oo ) F" :=
  (\big [+%E /0%E]_(0 ≤ i <oo ) F%E) : ereal_scope.

Section partial_esum.
Local Open Scope ereal_scope.

Variables (R : numDomainType) (u_ : (\bar R )^nat).

Definition eseries : (\bar R )^nat := [sequence \sum_(0 ≤ k < n ) u_ k ]_n.
Definition etelescope : (\bar R )^nat := [sequence u_ n.+1 - u_ n ]_n.

Lemma eseriesEnat : eseries = [sequence \sum_(0 ≤ k < n ) u_ k ]_n.

Lemma eseriesEord : eseries = [sequence \sum_(k < n ) u_ k ]_n.

Lemma eseriesSr n : eseries n.+1 = eseries n + u_ n.

Lemma eseriesS n : eseries n.+1 = u_ n + eseries n.

Lemma eseriesSB (n : nat) :
  eseries n \is a fin_num → eseries n.+1 - eseries n = u_ n.

Lemma eseries_addn m n : eseries (n + m)%N = eseries m + \sum_(m ≤ k < n + m ) u_ k.

Lemma sub_eseries_geq m n : (m ≤ n)%N → eseries m \is a fin_num →
  eseries n - eseries m = \sum_(m ≤ k < n ) u_ k.

Lemma sub_eseries m n : eseries m \is a fin_num → eseries n \is a fin_num →
  eseries n - eseries m = if (m ≤ n)%N then \sum_(m ≤ k < n ) u_ k
                        else - \sum_(n ≤ k < m ) u_ k.

Lemma sub_double_eseries n : eseries n \is a fin_num →
  eseries n.*2 - eseries n = \sum_(n ≤ k < n.*2) u_ k.

End partial_esum.

Arguments eseries {R} u_ n : simpl never.
Arguments etelescope {R} u_ n : simpl never.
Notation "[ 'series' E ]_ n" := (eseries [sequence E%E]_n) : ereal_scope.

Section eseries_ops.
Variable (R : numDomainType).
Local Open Scope ereal_scope.

Lemma eseriesD (f g : (\bar R )^nat) : eseries (f \+ g) = eseries f \+ eseries g.

End eseries_ops.

Section sequences_ereal_realDomainType.
Local Open Scope ereal_scope.
Variable T : realDomainType.
Implicit Types u : (\bar T )^nat.

Lemma ereal_nondecreasing_opp u_ :
  nondecreasing_seq (-%E \o u_) = nonincreasing_seq u_.

End sequences_ereal_realDomainType.

Section sequences_ereal.
Local Open Scope ereal_scope.

Lemma ereal_cvg_abs0 (R : realFieldType) (f : (\bar R )^nat) :
  abse \o f --> 0 → f --> 0.

Lemma ereal_cvg_ge0 (R : realFieldType) (f : (\bar R )^nat) (a : \bar R) :
  (∀ n, 0 ≤ f n ) → f --> a → 0 ≤ a.

Lemma ereal_lim_ge (R : realFieldType) x (u_ : (\bar R )^nat) : cvg u_ →
  (\∀ n \near \oo , x ≤ u_ n ) → x ≤ lim u_.

Lemma ereal_lim_le (R : realFieldType) x (u_ : (\bar R )^nat) : cvg u_ →
  (\∀ n \near \oo , u_ n ≤ x ) → lim u_ ≤ x.

Lemma cvgPpinfty_lt (R : realFieldType) (u_ : R ^nat) :
  u_ --> +oo%R ↔ ∀ A, \∀ n \near \oo , (A < u_ n)%R.

Lemma dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) :
  u_ --> +oo%R → [sequence (u_ n )%:E ]_n --> +oo.

Lemma ereal_cvg_real (R : realFieldType) (f : (\bar R )^nat) a :
  {near \oo , ∀ x, f x \is a fin_num } ∧
  (fine \o f --> a ) ↔ f --> a %:E.

Lemma ereal_nondecreasing_cvg (R : realType) (u_ : (\bar R )^nat) :
  nondecreasing_seq u_ → u_ --> ereal_sup (u_ @` setT).

Lemma ereal_nondecreasing_is_cvg (R : realType) (u_ : (\bar R ) ^nat) :
  nondecreasing_seq u_ → cvg u_.

Lemma ereal_nonincreasing_cvg (R : realType) (u_ : (\bar R )^nat) :
  nonincreasing_seq u_ → u_ --> ereal_inf (u_ @` setT).

Lemma ereal_nonincreasing_is_cvg (R : realType) (u_ : (\bar R ) ^nat) :
  nonincreasing_seq u_ → cvg u_.

NB: see also nondecreasing_series