(* 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.

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

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

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

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.

Section sequences_patched.

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) :
  (∀ n, 0 ≤ u_ n) → nondecreasing_seq (series u_).

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

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

Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat)
  (P : pred nat) : (∀ n, P n → 0 ≤ u_ n) →
  nondecreasing_seq (fun n ⇒ \sum_(0 ≤ i < n | P i) u_ i).

Lemma ereal_series_cond (R : realFieldType) (f : (\bar R)^nat) k P :
  \sum_(k ≤ i <oo | P i) f i = \sum_(i <oo | (k ≤ i)%N && P i) f i.

Lemma ereal_series (R : realFieldType) (f : (\bar R)^nat) k :
  \sum_(k ≤ i <oo) f i = \sum_(i <oo | (k ≤ i)%N) f i.

Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat)
  (P : pred nat) k : (∀ n, P n → 0 ≤ u_ n) →
  \sum_(0 ≤ i < k | P i) u_ i ≤ \sum_(i <oo | P i) u_ i.

Lemma is_cvg_ereal_nneg_natsum_cond (R : realType) m (u_ : (\bar R)^nat)
  (P : pred nat) : (∀ n, (m ≤ n)%N → P n → 0 ≤ u_ n) →
  cvg (fun n ⇒ \sum_(m ≤ i < n | P i) u_ i).

Lemma is_cvg_nneseries_cond (R : realType) (u_ : (\bar R)^nat)
  (P : pred nat) : (∀ n, P n → 0 ≤ u_ n) →
  cvg (fun n ⇒ \sum_(0 ≤ i < n | P i) u_ i).

Lemma is_cvg_ereal_nneg_natsum (R : realType) m (u_ : (\bar R)^nat) :
  (∀ n, (m ≤ n)%N → 0 ≤ u_ n) → cvg (fun n ⇒ \sum_(m ≤ i < n) u_ i).

Lemma is_cvg_nneseries (R : realType) (u_ : (\bar R)^nat)
  (P : pred nat) : (∀ n, P n → 0 ≤ u_ n) →
  cvg (fun n ⇒ \sum_(0 ≤ i < n | P i) u_ i).
Arguments is_cvg_nneseries {R}.

Lemma nneseriesrM (R : realType) (f : nat → \bar R) (P : pred nat) x :
  (∀ i, P i → 0 ≤ f i)%E →
  (\sum_(i <oo | P i) (x%:E × f i) = x%:E × \sum_(i <oo | P i) f i)%E.

Lemma nneseries_lim_ge0 (R : realType) (u_ : (\bar R)^nat) (P : pred nat) :
  (∀ n, P n → 0 ≤ u_ n) → 0 ≤ \sum_(i <oo | P i) u_ i.

Lemma adde_def_nneseries (R : realType) (f g : (\bar R)^nat)
    (P Q : pred nat) :
  (∀ n, P n → 0 ≤ f n) → (∀ n, Q n → 0 ≤ g n) →
  (\sum_(i <oo | P i) f i) +? (\sum_(i <oo | Q i) g i).

Lemma nneseries_pinfty (R : realType) (u_ : (\bar R)^nat)
  (P : pred nat) k : (∀ n, P n → 0 ≤ u_ n) → P k →
  u_ k = +oo → \sum_(i <oo | P i) u_ i = +oo.

Lemma ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R)^nat) :
  u_ --> +oo ↔ (∀ A, (0 < A)%R → \∀ n \near \oo, A%:E ≤ u_ n).

Lemma ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R)^nat) :
  u_ --> -oo ↔ (∀ A, (A < 0)%R → \∀ n \near \oo, u_ n ≤ A%:E).

Lemma ereal_squeeze (R : realType) (f g h : (\bar R)^nat) :
  (\∀ x \near \oo, f x ≤ g x ≤ h x) → ∀ (l : \bar R),
  f --> l → h --> l → g --> l.

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

Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) :
  (∀ i, P i → 0 ≤ u i) → (∀ n, P n → u n ≤ v n) →
  \sum_(i <oo | P i) u i ≤ \sum_(i <oo | P i) v i.

Lemma ereal_cvgD_pinfty_fin (R : realFieldType) (f g : (\bar R)^nat) b :
  f --> +oo → g --> b%:E → f \+ g --> +oo.

Lemma ereal_cvgD_ninfty_fin (R : realFieldType) (f g : (\bar R)^nat) b :
  f --> -oo → g --> b%:E → f \+ g --> -oo.

Lemma ereal_cvgD_pinfty_pinfty (R : realFieldType) (f g : (\bar R)^nat) :
  f --> +oo → g --> +oo → f \+ g --> +oo.

Lemma ereal_cvgD_ninfty_ninfty (R : realFieldType) (f g : (\bar R)^nat) :
  f --> -oo → g --> -oo → f \+ g --> -oo.

Lemma ereal_cvgD (R : realFieldType) (f g : (\bar R)^nat) a b :
  a +? b → f --> a → g --> b → f \+ g --> a + b.

Section nneseries_split.

Let lim_shift_cst (R : realFieldType) (u : (\bar R) ^nat) (l : \bar R) :
  cvg u → (∀ n, 0 ≤ u n) → -oo < l → lim (fun x ⇒ l + u x) = l + lim u.

Let near_eq_lim (R : realFieldType) (f g : nat → \bar R) :
  cvg g → {near \oo, f =1 g} → lim f = lim g.

Lemma nneseries_split (R : realType) (f : nat → \bar R) n :
  (∀ k, 0 ≤ f k) →
  \sum_(k <oo) f k = \sum_(k < n) f k + \sum_(n ≤ k <oo) f k.

End nneseries_split.

Lemma ereal_cvgB (R : realFieldType) (f g : (\bar R)^nat) a b :
  a +? - b → f --> a → g --> b → f \- g --> a - b.

Lemma ereal_is_cvgD (R : realFieldType) (u v : (\bar R)^nat) :
  lim u +? lim v → cvg u → cvg v → cvg (u \+ v).

Lemma ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) :
  k \is a fin_num → (fun x ⇒ f x - k) --> 0 ↔ f --> k.

Lemma ereal_limD (R : realFieldType) (f g : (\bar R)^nat) :
  cvg f → cvg g → lim f +? lim g →
  lim (f \+ g) = lim f + lim g.

Lemma ereal_cvgM_gt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b :
  (0 < b)%R → f --> +oo → g --> b%:E → f \* g --> +oo.

Lemma ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b :
  (b < 0)%R → f --> +oo → g --> b%:E → f \* g --> -oo.

Lemma ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b :
  (0 < b)%R → f --> -oo → g --> b%:E → f \* g --> -oo.

Lemma ereal_cvgM_lt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b :
  (b < 0)%R → f --> -oo → g --> b%:E → f \* g --> +oo.

Lemma ereal_cvgM (R : realType) (f g : (\bar R) ^nat) (a b : \bar R) :
 a *? b → f --> a → g --> b → f \* g --> a × b.

Lemma ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I)
    (f : I → (\bar R)^nat) (l : I → \bar R) (P : pred I) :
  (∀ k n, P k → 0 ≤ f k n) →
  (∀ k, P k → f k --> l k) →
  (fun n ⇒ \sum_(k <- r | P k) f k n) --> \sum_(k <- r | P k) l k.

Lemma nneseriesD (R : realType) (f g : nat → \bar R) (P : pred nat) :
  (∀ i, P i → 0 ≤ f i) → (∀ i, P i → 0 ≤ g i) →
  \sum_(i <oo | P i) (f i + g i) =
  \sum_(i <oo | P i) f i + \sum_(i <oo | P i) g i.

Lemma nneseries0 (R : realFieldType) (f : (\bar R)^nat) (P : pred nat) :
  (∀ i, P i → f i = 0) → \sum_(i <oo | P i) f i = 0.

Lemma nneseries_pred0 (R : realFieldType) (P : pred nat) (f : nat → \bar R) :
  P =1 xpred0 → \sum_(i <oo | P i) f i = 0.

Lemma eq_nneseries (R : realFieldType) (f g : (\bar R)^nat) (P : pred nat) :
  (∀ i, P i → f i = g i) → \sum_(i <oo | P i) f i = \sum_(i <oo | P i) g i.

Lemma nneseries_sum_nat (R : realType) n (f : nat → nat → \bar R) :
  (∀ i j, 0 ≤ f i j) →
  \sum_(j <oo) (\sum_(0 ≤ i < n) f i j) =
  \sum_(0 ≤ i < n) (\sum_(j <oo) (f i j)).

Lemma nneseries_sum I (r : seq I) (P : {pred I})
    [R : realType] [f : I → nat → \bar R] :
    (∀ i j, P i → 0 ≤ f i j) →
  \sum_(j <oo) \sum_(i <- r | P i) f i j = \sum_(i <- r | P i) \sum_(j <oo) f i j.

Lemma lte_lim (R : realFieldType) (u : (\bar R)^nat) (M : R) :
  nondecreasing_seq u → cvg u → M%:E < lim u →
  \∀ n \near \oo, M%:E ≤ u n.

Lemma lim_mkord (R : realFieldType) (P : {pred nat}) (f : (\bar R)^nat) :
  lim (fun n ⇒ \sum_(k < n | P k) f k)%E = \sum_(k <oo | P k) f k.

Lemma nneseries_mkcond [R : realFieldType] [P : pred nat] (f : nat → \bar R) :
  \sum_(i <oo | P i) f i = \sum_(i <oo) if P i then f i else 0.

End sequences_ereal.

Definition sdrop T (u : T^nat) n := [set u k | k in [set k | k ≥ n]]%N.

Section sdrop.
Variables (d : unit) (R : porderType d).
Implicit Types (u : R^o^nat).

Lemma has_lbound_sdrop u : has_lbound (range u) →
  ∀ m, has_lbound (sdrop u m).

Lemma has_ubound_sdrop u : has_ubound (range u) →
  ∀ m, has_ubound (sdrop u m).

End sdrop.

Section sups_infs.
Variable R : realType.
Implicit Types (r : R) (u : R^o^nat).

Definition sups u := [sequence sup (sdrop u n)]_n.

Definition infs u := [sequence inf (sdrop u n)]_n.

Lemma supsN u : sups (-%R \o u) = - infs u.

Lemma infsN u : infs (-%R \o u) = - sups u.

Lemma nonincreasing_sups u : has_ubound (range u) →
  nonincreasing_seq (sups u).

Lemma nondecreasing_infs u : has_lbound (range u) →
  nondecreasing_seq (infs u).

Lemma is_cvg_sups u : cvg u → cvg (sups u).

Lemma is_cvg_infs u : cvg u → cvg (infs u).

Lemma infs_le_sups u n : cvg u → infs u n ≤ sups u n.

Lemma cvg_sups_inf u : has_ubound (range u) → has_lbound (range u) →
  sups u --> inf (range (sups u)).

Lemma cvg_infs_sup u : has_ubound (range u) → has_lbound (range u) →
  infs u --> sup (range (infs u)).

Lemma sups_preimage T (D : set T) r (f : (T → R)^nat) n :
  (∀ t, D t → has_ubound (range (f ^~ t))) →
  D `&` (fun x ⇒ sups (f ^~x) n) @^-1` `]r, +oo[%classic =
  D `&` \bigcup_(k in [set k | n ≤ k]%N) f k @^-1` `]r, +oo[.

Lemma infs_preimage T (D : set T) r (f : (T → R)^nat) n :
  (∀ t, D t → has_lbound (range (f ^~ t))) →
  D `&` (fun x ⇒ infs (f ^~ x) n) @^-1` `]-oo, r[ =
  D `&` \bigcup_(k in [set k | n ≤ k]%N) f k @^-1` `]-oo, r[.

Lemma bounded_fun_has_lbound_sups u :
  bounded_fun u → has_lbound (range (sups u)).

Lemma bounded_fun_has_ubound_infs u :
  bounded_fun u → has_ubound (range (infs u)).

End sups_infs.

Section lim_sup_lim_inf.
Variable R : realType.
Implicit Types (r : R) (u v : R^o^nat).

Definition lim_sup u := lim (sups u).

Definition lim_inf u := lim (infs u).

Lemma lim_infN u : cvg u → lim_inf (-%R \o u) = - lim_sup u.

Lemma lim_supE u : bounded_fun u → lim_sup u = inf (range (sups u)).

Lemma lim_infE u : bounded_fun u → lim_inf u = sup (range (infs u)).

Lemma lim_inf_le_lim_sup u : cvg u → lim_inf u ≤ lim_sup u.

Lemma cvg_lim_inf_sup u l : u --> l → (lim_inf u = l) × (lim_sup u = l).

Lemma cvg_lim_infE u : cvg u → lim_inf u = lim u.

Lemma cvg_lim_supE u : cvg u → lim_sup u = lim u.

Lemma cvg_sups u l : u --> l → (sups u) --> (l : R^o).

Lemma cvg_infs u l : u --> l → (infs u) --> (l : R^o).

Lemma le_lim_supD u v :
  bounded_fun u → bounded_fun v → lim_sup (u \+ v) ≤ lim_sup u + lim_sup v.

Lemma le_lim_infD u v :
  bounded_fun u → bounded_fun v → lim_inf u + lim_inf v ≤ lim_inf (u \+ v).

Lemma lim_supD u v : cvg u → cvg v → lim_sup (u \+ v) = lim_sup u + lim_sup v.

Lemma lim_infD u v : cvg u → cvg v → lim_inf (u \+ v) = lim_inf u + lim_inf v.

End lim_sup_lim_inf.

Section esups_einfs.
Variable R : realType.
Implicit Types (u : (\bar R)^nat).
Local Open Scope ereal_scope.

Definition esups u := [sequence ereal_sup (sdrop u n)]_n.

Definition einfs u := [sequence ereal_inf (sdrop u n)]_n.

Lemma esupsN u : esups (-%E \o u) = -%E \o einfs u.

Lemma einfsN u : einfs (-%E \o u) = -%E \o esups u.

Lemma nonincreasing_esups u : nonincreasing_seq (esups u).

Lemma nondecreasing_einfs u : nondecreasing_seq (einfs u).

Lemma einfs_le_esups u n : einfs u n ≤ esups u n.

Lemma cvg_esups_inf u : esups u --> ereal_inf (range (esups u)).

Lemma is_cvg_esups u : cvg (esups u).

Lemma cvg_einfs_sup u : einfs u --> ereal_sup (range (einfs u)).

Lemma is_cvg_einfs u : cvg (einfs u).

Lemma esups_preimage T (a : \bar R) (f : (T → \bar R)^nat) n :
  (fun x ⇒ esups (f^~x) n) @^-1` `]a, +oo[ =
  \bigcup_(k in [set k | n ≤ k]%N) f k @^-1` `]a, +oo[.

Lemma einfs_preimage T (a : \bar R) (f : (T → \bar R)^nat) n :
  (fun x ⇒ einfs (f^~x) n) @^-1` `[a, +oo[%classic =
  \bigcap_(k in [set k | n ≤ k]%N) f k @^-1` `[a, +oo[%classic.

End esups_einfs.

Section elim_sup_inf.
Local Open Scope ereal_scope.
Variable R : realType.
Implicit Types (u v : (\bar R)^nat) (l : \bar R).

Definition elim_sup u := lim (esups u).

Definition elim_inf u := lim (einfs u).

Lemma elim_inf_shift u l : l \is a fin_num →
  elim_inf (fun x ⇒ l + u x) = l + elim_inf u.

Lemma elim_sup_le_cvg u l : elim_sup u ≤ l → (∀ n, l ≤ u n) → u --> l.

Lemma elim_infN u : elim_inf (-%E \o u) = - elim_sup u.

Lemma elim_supN u : elim_sup (-%E \o u) = - elim_inf u.

Lemma elim_inf_sup u : elim_inf u ≤ elim_sup u.

Lemma cvg_ninfty_elim_inf_sup u : u --> -oo →
  (elim_inf u = -oo) × (elim_sup u = -oo).

Lemma cvg_ninfty_einfs u : u --> -oo → einfs u --> -oo.

Lemma cvg_ninfty_esups u : u --> -oo → esups u --> -oo.

Lemma cvg_pinfty_einfs u : u --> +oo → einfs u --> +oo.

Lemma cvg_pinfty_esups u : u --> +oo → esups u --> +oo.

Lemma cvg_esups u l : u --> l → esups u --> l.

Lemma cvg_einfs u l : u --> l → einfs u --> l.

Lemma cvg_elim_inf_sup u l : u --> l → (elim_inf u = l) × (elim_sup u = l).

Lemma is_cvg_elim_infE u : cvg u → elim_inf u = lim u.

Lemma is_cvg_elim_supE u : cvg u → elim_sup u = lim u.

End elim_sup_inf.