Module mathcomp.analysis.sequences

From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import set_interval.
Require Import reals ereal signed topology normedtype landau.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
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) :
  (forall n, u_ n <= u_ n.+1)%O <-> nondecreasing_seq u_.

Lemma nonincreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) :
  (forall n, u_ n >= u_ n.+1)%O <-> nonincreasing_seq u_.

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

Lemma decreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) :
  (forall 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) :
  (forall x, nondecreasing_seq (f ^~ x)) ->
  (forall x, nondecreasing_seq (g ^~ x)) ->
  (forall x, nondecreasing_seq ((f \+ g) ^~ x)).

Local Notation eqolimn := (@eqolim _ _ _ eventually_filter).
Local Notation eqolimPn := (@eqolimP _ _ _ eventually_filter).


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.

Lemma seqDUIE (S : set T) (F : (set T)^nat) :
  seqDU (fun n => S `&` F n) = (fun n => S `&` F n `\` \bigcup_(i < n) F i).

End seqDU.
Arguments trivIset_seqDU {T} F.
#[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 seqDU_seqD 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 ->
  forall 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_ :
  cvgn [sequence if (n <= N)%nat then f n else u_ n]_n = cvgn u_.

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

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

End NatShift.

Variables (V : topologicalType).

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

End sequences_patched.

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

Lemma __deprecated__squeeze T (f g h : T -> R) (a : filter_on T) :
  (\forall x \near a, f x <= g x <= h x) -> forall (l : R),
  f @ a --> l -> h @ a --> l -> g @ a --> l.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `squeeze_cvgr`")]
Notation squeeze := __deprecated__squeeze (only parsing).

Lemma __deprecated__cvgPpinfty (u_ : R ^nat) :
  u_ @ \oo --> +oo <-> forall A, \forall n \near \oo, A <= u_ n.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgryPge`, and generalized to any filter")]
Notation cvgPpinfty := __deprecated__cvgPpinfty (only parsing).

Lemma __deprecated__cvgNpinfty u_ : (- u_ @ \oo --> +oo) = (u_ @ \oo --> -oo).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgNry` instead")]
Notation cvgNpinfty := __deprecated__cvgNpinfty (only parsing).

Lemma __deprecated__cvgNninfty u_ : (- u_ @ \oo --> -oo) = (u_ @ \oo --> +oo).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgNrNy` instead")]
Notation cvgNninfty := __deprecated__cvgNninfty (only parsing).

Lemma __deprecated__cvgPninfty (u_ : R ^nat) :
  u_ @ \oo --> -oo <-> forall A, \forall n \near \oo, A >= u_ n.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrNyPle`, and generalized to any filter")]
Notation cvgPninfty := __deprecated__cvgPninfty (only parsing).

Lemma __deprecated__ger_cvg_pinfty u_ v_ : (\forall n \near \oo, u_ n <= v_ n) ->
  u_ @ \oo --> +oo -> v_ @ \oo --> +oo.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `ger_cvgy`, and generalized to any filter")]
Notation ger_cvg_pinfty := __deprecated__ger_cvg_pinfty (only parsing).

Lemma __deprecated__ler_cvg_ninfty v_ u_ : (\forall n \near \oo, u_ n <= v_ n) ->
  v_ @ \oo --> -oo -> u_ @ \oo --> -oo.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `ler_cvgNy`, and generalized to any filter")]
Notation ler_cvg_ninfty := __deprecated__ler_cvg_ninfty (only parsing).

Lemma __deprecated__lim_ge x u : cvg (u @ \oo) ->
  (\forall n \near \oo, x <= u n) -> x <= lim (u @ \oo).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `limr_ge`, and generalized to any proper filter")]
Notation lim_ge := __deprecated__lim_ge (only parsing).

Lemma __deprecated__lim_le x u : cvg (u @ \oo) ->
  (\forall n \near \oo, x >= u n) -> x >= lim (u @ \oo).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `limr_le`, and generalized to any proper filter")]
Notation lim_le := __deprecated__lim_le (only parsing).

Lemma lt_lim u (M : R) : nondecreasing_seq u ->
  cvgn u -> M < limn u -> \forall n \near \oo, M <= u n.

Lemma nonincreasing_cvgn_ge u_ : nonincreasing_seq u_ -> cvgn u_ ->
  forall n, limn u_ <= u_ n.

Lemma nondecreasing_cvgn_le u_ : nondecreasing_seq u_ -> cvgn u_ ->
  forall n, u_ n <= limn u_.

Lemma cvg_has_ub u_ : cvgn u_ -> has_ubound [set `|u_ n| | n in setT].

Lemma cvg_has_sup u_ : cvgn u_ -> has_sup (u_ @` setT).

Lemma cvg_has_inf u_ : cvgn u_ -> has_inf (u_ @` setT).

Lemma __deprecated__cvgPpinfty_lt (u_ : R ^nat) :
  u_ @ \oo --> +oo%R <-> forall A, \forall n \near \oo, (A < u_ n)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgryPgt`, and generalized to any proper filter")]
Notation cvgPpinfty_lt := __deprecated__cvgPpinfty_lt (only parsing).

Lemma __deprecated__cvgPninfty_lt (u_ : R ^nat) :
  u_ @ \oo --> -oo%R <-> forall A, \forall n \near \oo, (A > u_ n)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrNyPlt`, and generalized to any proper filter")]
Notation cvgPninfty_lt := __deprecated__cvgPninfty_lt (only parsing).

Lemma __deprecated__cvgPpinfty_near (u_ : R ^nat) :
  u_ @ \oo --> +oo%R <-> \forall A \near +oo, \forall n \near \oo, (A <= u_ n)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgryPgey`, and generalized to any proper filter")]
Notation cvgPpinfty_near := __deprecated__cvgPpinfty_near (only parsing).

Lemma __deprecated__cvgPninfty_near (u_ : R ^nat) :
  u_ @ \oo --> -oo%R <-> \forall A \near -oo, \forall n \near \oo, (A >= u_ n)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrNyPleNy`, and generalized to any proper filter")]
Notation cvgPninfty_near := __deprecated__cvgPninfty_near (only parsing).

Lemma __deprecated__cvgPpinfty_lt_near (u_ : R ^nat) :
  u_ @ \oo --> +oo%R <-> \forall A \near +oo, \forall n \near \oo, (A < u_ n)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgryPgty`, and generalized to any proper filter")]
Notation cvgPpinfty_lt_near := __deprecated__cvgPpinfty_lt_near (only parsing).

Lemma __deprecated__cvgPninfty_lt_near (u_ : R ^nat) :
  u_ @ \oo --> -oo%R <-> \forall A \near -oo, \forall n \near \oo, (A > u_ n)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrNyPltNy`, and generalized to any proper filter")]
Notation cvgPninfty_lt_near := __deprecated__cvgPninfty_lt_near (only parsing).

End sequences_R_lemmas_realFieldType.
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nonincreasing_cvgn_ge`")]
Notation nonincreasing_cvg_ge := nonincreasing_cvgn_ge (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nondecreasing_cvgn_le`")]
Notation nondecreasing_cvg_le := nondecreasing_cvgn_le (only parsing).

Lemma __deprecated__invr_cvg0 (R : realFieldType) (u : R^nat) :
  (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> 0) <-> (u @ \oo --> +oo).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `gtr0_cvgV0` and generalized")]
Notation invr_cvg0 := __deprecated__invr_cvg0 (only parsing).

Lemma __deprecated__invr_cvg_pinfty (R : realFieldType) (u : R^nat) :
  (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> +oo) <-> (u @ \oo--> 0).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrVy` and generalized")]
Notation invr_cvg_pinfty := __deprecated__invr_cvg_pinfty (only parsing).

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 : cvgn (series (- f)) = cvgn (series f).

Lemma lim_seriesN f : cvg (series f @ \oo) ->
  limn (series (- f)) = - limn (series f).

Lemma is_cvg_seriesZ f k : cvgn (series f) -> cvgn (series (k *: f)).

Lemma lim_seriesZ f k : cvgn (series f) ->
  limn (series (k *: f)) = k *: limn (series f).

Lemma is_cvg_seriesD f g :
  cvgn (series f) -> cvgn (series g) -> cvgn (series (f + g)).

Lemma lim_seriesD f g : cvgn (series f) -> cvgn (series g) ->
  limn (series (f + g)) = limn (series f) + limn (series g).

Lemma is_cvg_seriesB f g :
  cvgn (series f) -> cvgn (series g) -> cvgn (series (f - g)).

Lemma lim_seriesB f g : cvg (series f @ \oo) -> cvg (series g @ \oo) ->
  limn (series (f - g)) = limn (series f) - limn (series g).

End partial_sum_numFieldType.

Lemma lim_series_le (V : realFieldType) (f g : V ^nat) :
  cvgn (series f) -> cvgn (series g) -> (forall n, f n <= g n) ->
  limn (series f) <= limn (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_ :
  cvgn [sequence \sum_(N <= k < n) u_ k]_n = cvgn (series u_).

End series_patched.

Section sequences_R_lemmas.
Variable R : realType.

Lemma nondecreasing_cvgn (u_ : R ^nat) :
    nondecreasing_seq u_ -> has_ubound (range u_) ->
  u_ @ \oo --> sup (range u_).

Lemma nondecreasing_is_cvgn (u_ : R ^nat) :
  nondecreasing_seq u_ -> has_ubound (range u_) -> cvgn u_.

Lemma nondecreasing_dvgn_lt (u_ : R ^nat) :
  nondecreasing_seq u_ -> ~ cvgn u_ -> u_ @ \oo --> +oo.

Lemma near_nondecreasing_is_cvgn (u_ : R ^nat) (M : R) :
    {near \oo, nondecreasing_seq u_} -> (\forall n \near \oo, u_ n <= M) ->
  cvgn u_.

Lemma nonincreasing_cvgn (u_ : R ^nat) :
    nonincreasing_seq u_ -> has_lbound (range u_) ->
  u_ @ \oo --> inf (u_ @` setT).

Lemma nonincreasing_is_cvgn (u_ : R ^nat) :
  nonincreasing_seq u_ -> has_lbound (range u_) -> cvgn u_.

Lemma near_nonincreasing_is_cvgn (u_ : R ^nat) (m : R) :
    {near \oo, nonincreasing_seq u_} -> (\forall n \near \oo, m <= u_ n) ->
  cvgn u_.

Lemma adjacent (u_ v_ : R ^nat) : nondecreasing_seq u_ -> nonincreasing_seq v_ ->
  v_ - u_ @ \oo --> (0 : R) ->
  [/\ limn v_ = limn u_, cvgn u_ & cvgn v_].

End sequences_R_lemmas.
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nonincreasing_cvgn`")]
Notation nonincreasing_cvg := nonincreasing_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nondecreasing_cvgn`")]
Notation nondecreasing_cvg := nondecreasing_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nonincreasing_is_cvgn`")]
Notation nonincreasing_is_cvg := nonincreasing_is_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nondecreasing_is_cvgn`")]
Notation nondecreasing_is_cvg := nondecreasing_is_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `nondecreasing_dvgn_lt`")]
Notation nondecreasing_dvg_lt := nondecreasing_dvgn_lt (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `near_nondecreasing_is_cvgn`")]
Notation near_nondecreasing_is_cvg := near_nondecreasing_is_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `near_nonincreasing_is_cvgn`")]
Notation near_nonincreasing_is_cvg := near_nonincreasing_is_cvgn (only parsing).

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 R @ \oo --> 0.

Lemma cvge_harmonic {R : archiFieldType} : (EFin \o @harmonic R) @ \oo --> 0%E.

Lemma dvg_harmonic (R : numFieldType) : ~ cvgn (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_ @ \oo --> l ->
  arithmetic_mean u_ @ \oo --> 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 @ \oo --> (0 : R) ->
  [sequence n.+1%:R^-1 * series u_ n]_n @ \oo --> (0 : R).

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

End cesaro_converse.

Section series_convergence.

Lemma cvg_series_cvg_0 (K : numFieldType) (V : normedModType K) (u_ : V ^nat) :
  cvgn (series u_) -> u_ @ \oo --> (0 : V).

Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) (P : pred nat) :
  (forall 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) :
  (forall 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 --> +oo.

Lemma cvg_expr (R : archiFieldType) (z : R) :
  `|z| < 1 -> (GRing.exp z : R ^nat) @ \oo --> (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) @ \oo --> (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) @ \oo --> (r / 2 ^+ n : R^o).
Arguments cvg_geometric_series_half {R} _ _.

Lemma geometric_partial_tail {R : fieldType} (n m : nat) (x : R) :
  \sum_(m <= i < m + n) x ^+ i = series (geometric (x ^+ m) x) n.

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

Lemma is_cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 ->
  cvgn (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) :
  (forall n, 0 <= u_ n) -> [normed series u_] = series u_.

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

Lemma series_le_cvg (R : realType) (u_ v_ : R ^nat) :
  (forall n, 0 <= u_ n) -> (forall n, 0 <= v_ n) ->
  (forall n, u_ n <= v_ n) ->
  cvgn (series v_) -> cvgn (series u_).

Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) :
  cvgn [normed series u_] -> cvgn (series u_).

Lemma lim_series_norm {R : realType} (V : completeNormedModType R) (f : V ^nat) :
    cvgn [normed series f] ->
  `|limn (series f)| <= limn [normed series f].

Section series_linear.

Lemma cvg_series_bounded (R : realFieldType) (f : R ^nat) :
  cvgn (series f) -> bounded_fun f.

Lemma cvg_to_0_linear (R : realFieldType) (f : R -> R) K (k : R) :
  0 < k -> (forall 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 -> cvgn (series f) ->
  (forall r, 0 < `|r| < k -> forall n, `|g r n| <= f n * `| r |) ->
  limn (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.

Local Notation exp := exp_coeff.

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 -> cvgn (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 : cvgn (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 : cvgn (series (exp x)).

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

End exponential_series.

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


Lemma __deprecated__nat_dvg_real (R : realType) (u_ : nat ^nat) :
  u_ @ \oo --> \oo -> ([sequence (u_ n)%:R : R^o]_n @ \oo --> +oo)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrnyP` and generalized")]
Notation nat_dvg_real := __deprecated__nat_dvg_real (only parsing).

Lemma __deprecated__nat_cvgPpinfty (u : nat^nat) :
  u @ \oo --> \oo <-> forall A, \forall n \near \oo, (A <= u n)%N.
#[deprecated(since="mathcomp-analysis 0.6.0",
      note="renamed to `cvgnyPge` and generalized")]
Notation nat_cvgPpinfty:= __deprecated__nat_cvgPpinfty (only parsing).

Lemma nat_nondecreasing_is_cvg (u_ : nat^nat) :
  nondecreasing_seq u_ -> has_ubound (range u_) -> cvgn 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) : cvgn (nseries u) ->
  \forall n \near \oo, u n = 0%N.

Lemma dvg_nseries (u : nat^nat) : ~ cvgn (nseries u) ->
  nseries u @ \oo --> \oo.


Notation "\big [ op / idx ]_ ( m <= i <oo | P ) F" :=
  (limn (fun n => (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope.
Notation "\big [ op / idx ]_ ( m <= i <oo ) F" :=
  (limn (fun n => (\big[ op / idx ]_(m <= i < n) F))) : big_scope.
Notation "\big [ op / idx ]_ ( i <oo | P ) F" :=
  (limn (fun n => (\big[ op / idx ]_(i < n | P) F))) : big_scope.
Notation "\big [ op / idx ]_ ( i <oo ) F" :=
  (limn (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_oppn u_ :
  nondecreasing_seq (-%E \o u_) = nonincreasing_seq u_.

End sequences_ereal_realDomainType.
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `ereal_nondecreasing_oppn`")]
Notation ereal_nondecreasing_opp := ereal_nondecreasing_oppn (only parsing).

Section sequences_ereal.
Local Open Scope ereal_scope.

Lemma __deprecated__ereal_cvg_abs0 (R : realFieldType) (f : (\bar R)^nat) :
  abse \o f @ \oo --> 0 -> f @ \oo --> 0.

Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) :
  (forall n, 0 <= f n) -> f @ \oo --> a -> 0 <= a.

Lemma __deprecated__ereal_lim_ge (R : realFieldType) x (u_ : (\bar R)^nat) :
  cvgn u_ -> (\forall n \near \oo, x <= u_ n) -> x <= limn u_.

Lemma __deprecated__ereal_lim_le (R : realFieldType) x (u_ : (\bar R)^nat) :
  cvgn u_ -> (\forall n \near \oo, u_ n <= x) -> limn u_ <= x.

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

Lemma __deprecated__ereal_cvg_real (R : realFieldType) (f : (\bar R)^nat) a :
  {near \oo, forall x, f x \is a fin_num} /\
  (fine \o f @ \oo --> a) <-> f @ \oo --> a%:E.

Lemma ereal_nondecreasing_cvgn (R : realType) (u_ : (\bar R)^nat) :
  nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (range u_).

Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
  nondecreasing_seq u_ -> cvgn u_.

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

Lemma ereal_nonincreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
  nonincreasing_seq u_ -> cvgn u_.

Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat)
  (P : pred nat) : (forall n, P n -> 0 <= u_ n) ->
  nondecreasing_seq (fun n => \sum_(0 <= i < n | P i) u_ i).

Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) :
  f = g -> limn f = limn g.

Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N :
  \sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i.

Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q :
  \sum_(i <oo | P i && Q i) f i = \sum_(i <oo | Q i) if P i then f i else 0.

Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q :
  \sum_(i <oo | P i && Q i) f i = \sum_(i <oo | P i) if Q i then f i else 0.

Lemma eq_eseriesr (R : numFieldType) (f g : (\bar R)^nat) (P : pred nat) {N} :
  (forall i, P i -> f i = g i) ->
  \sum_(N <= i <oo | P i) f i = \sum_(N <= i <oo | P i) g i.

Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) :
  P =1 Q -> \sum_(i <oo | P i) f i = \sum_(i <oo | Q i) f i.
Arguments eq_eseriesl {R P} Q.

Section ereal_series.
Variables (R : realFieldType) (f : (\bar R)^nat).
Implicit Types P : pred nat.

Lemma ereal_series_cond k P :
  \sum_(k <= i <oo | P i) f i = \sum_(i <oo | (k <= i)%N && P i) f i.

Lemma ereal_series k : \sum_(k <= i <oo) f i = \sum_(i <oo | (k <= i)%N) f i.

Lemma eseries0 P : (forall i, P i -> f i = 0) -> \sum_(i <oo | P i) f i = 0.

Lemma eseries_pred0 P : P =1 xpred0 -> \sum_(i <oo | P i) f i = 0.

End ereal_series.

Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k :
  (forall n, P n -> 0 <= u_ n) ->
  \sum_(0 <= i < k | P i) u_ i <= \sum_(i <oo | P i) u_ i.

Lemma eseries_pinfty (R : realFieldType) (u_ : (\bar R)^nat)
    (P : pred nat) k : (forall n, P n -> u_ n != -oo) -> P k ->
  u_ k = +oo -> \sum_(i <oo | P i) u_ i = +oo.

Section cvg_eseries.
Variable (R : realType) (u_ : (\bar R)^nat).
Implicit Type P : pred nat.

Lemma is_cvg_ereal_nneg_natsum_cond m P :
    (forall n, (m <= n)%N -> P n -> 0 <= u_ n) ->
  cvgn (fun n => \sum_(m <= i < n | P i) u_ i).

Lemma is_cvg_ereal_npos_natsum_cond m P :
    (forall n, (m <= n)%N -> P n -> u_ n <= 0) ->
  cvgn (fun n => \sum_(m <= i < n | P i) u_ i).

Lemma is_cvg_ereal_nneg_natsum m : (forall n, (m <= n)%N -> 0 <= u_ n) ->
  cvgn (fun n => \sum_(m <= i < n) u_ i).

Lemma is_cvg_ereal_npos_natsum m : (forall n, (m <= n)%N -> u_ n <= 0) ->
  cvgn (fun n => \sum_(m <= i < n) u_ i).

Lemma is_cvg_nneseries_cond P N : (forall n, P n -> 0 <= u_ n) ->
  cvgn (fun n => \sum_(N <= i < n | P i) u_ i).

Lemma is_cvg_npeseries_cond P N : (forall n, P n -> u_ n <= 0) ->
  cvgn (fun n => \sum_(N <= i < n | P i) u_ i).

Lemma is_cvg_nneseries P N : (forall n, P n -> 0 <= u_ n) ->
  cvgn (fun n => \sum_(N <= i < n | P i) u_ i).

Lemma is_cvg_npeseries P N : (forall n, P n -> u_ n <= 0) ->
  cvgn (fun n => \sum_(N <= i < n | P i) u_ i).

Lemma nneseries_ge0 P N : (forall n, P n -> 0 <= u_ n) ->
  0 <= \sum_(N <= i <oo | P i) u_ i.

Lemma npeseries_le0 P N : (forall n : nat, P n -> u_ n <= 0) ->
  \sum_(N <= i <oo | P i) u_ i <= 0.

End cvg_eseries.
Arguments is_cvg_nneseries {R}.
Arguments nneseries_ge0 {R u_ P} N.

Lemma nnseries_is_cvg {R : realType} (u : nat -> R) :
    (forall i, 0 <= u i)%R -> \sum_(k <oo) (u k)%:E < +oo ->
  cvgn (series u).

Lemma nneseriesZl (R : realType) (f : nat -> \bar R) (P : pred nat) x N :
  (forall i, P i -> 0 <= f i) ->
  (\sum_(N <= i <oo | P i) (x%:E * f i) = x%:E * \sum_(N <= i <oo | P i) f i).

Lemma adde_def_nneseries (R : realType) (f g : (\bar R)^nat)
    (P Q : pred nat) :
  (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) ->
  (\sum_(i <oo | P i) f i) +? (\sum_(i <oo | Q i) g i).

Lemma __deprecated__ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R)^nat) :
  u_ @ \oo --> +oo <-> (forall A, (0 < A)%R -> \forall n \near \oo, A%:E <= u_ n).

Lemma __deprecated__ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R)^nat) :
  u_ @ \oo --> -oo <-> (forall A, (A < 0)%R -> \forall n \near \oo, u_ n <= A%:E).

Lemma __deprecated__ereal_squeeze (R : realType) (f g h : (\bar R)^nat) :
  (\forall x \near \oo, f x <= g x <= h x) -> forall (l : \bar R),
  f @ \oo --> l -> h @ \oo --> l -> g @ \oo --> l.

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

Lemma lee_nneseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) N :
  (forall i, P i -> 0 <= u i) ->
  (forall n, P n -> u n <= v n) ->
  \sum_(N <= i <oo | P i) u i <= \sum_(N <= i <oo | P i) v i.

Lemma lee_npeseries (R : realType) (u v : (\bar R)^nat) (P : pred nat) :
  (forall i, P i -> u i <= 0) -> (forall n, P n -> v n <= u n) ->
  \sum_(i <oo | P i) v i <= \sum_(i <oo | P i) u i.

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

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

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

Lemma __deprecated__ereal_cvgD_ninfty_ninfty (R : realFieldType) (f g : (\bar R)^nat) :
  f @ \oo --> -oo -> g @ \oo --> -oo -> f \+ g @ \oo --> -oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
Notation ereal_cvgD_ninfty_ninfty := __deprecated__ereal_cvgD_ninfty_ninfty (only parsing).

Lemma __deprecated__ereal_cvgD (R : realFieldType) (f g : (\bar R)^nat) a b :
  a +? b -> f @ \oo --> a -> g @ \oo --> b -> f \+ g @ \oo --> a + b.

Lemma __deprecated__ereal_cvgB (R : realFieldType) (f g : (\bar R)^nat) a b :
  a +? - b -> f @ \oo --> a -> g @ \oo --> b -> f \- g @ \oo --> a - b.

Lemma __deprecated__ereal_is_cvgD (R : realFieldType) (u v : (\bar R)^nat) :
    limn u +? limn v -> cvgn u -> cvgn v -> cvgn (u \+ v).

Lemma __deprecated__ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) :
  k \is a fin_num -> (fun x => f x - k) @ \oo --> 0 <-> f @ \oo --> k.

Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) :
  cvgn f -> cvgn g -> limn f +? limn g ->
  limn (f \+ g) = limn f + limn g.

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

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

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

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

Lemma __deprecated__ereal_cvgM (R : realType) (f g : (\bar R) ^nat) (a b : \bar R) :
 a *? b -> f @ \oo --> a -> g @ \oo --> b -> f \* g @ \oo --> a * b.

Lemma __deprecated__ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I)
    (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) :
  (forall k n, P k -> 0 <= f k n) ->
  (forall k, P k -> f k @ \oo --> l k) ->
  (fun n => \sum_(k <- r | P k) f k n) @ \oo --> \sum_(k <- r | P k) l k.

Let lim_shift_cst (R : realFieldType) (u : (\bar R) ^nat) (l : \bar R) :
    cvgn u -> (forall n, 0 <= u n) -> -oo < l ->
  limn (fun x => l + u x) = l + limn u.

Section nneseries_split.

Let near_eq_lim (R : realFieldType) (f g : nat -> \bar R) :
  cvgn g -> {near \oo, f =1 g} -> limn f = limn g.

Lemma nneseries_split (R : realType) (f : nat -> \bar R) n :
  (forall k, 0 <= f k) ->
  \sum_(k <oo) f k = \sum_(k < n) f k + \sum_(n <= k <oo) f k.

End nneseries_split.

Lemma nneseries_tail_cvg (R : realType) (f : (\bar R)^nat) :
  \sum_(k <oo) f k < +oo -> (forall k, 0 <= f k) ->
  \sum_(N <= k <oo) f k @[N --> \oo] --> 0.

Lemma nneseriesD (R : realType) (f g : nat -> \bar R) (P : pred nat) :
  (forall i, P i -> 0 <= f i) -> (forall 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 nneseries_sum_nat (R : realType) n (f : nat -> nat -> \bar R) :
  (forall 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] : (forall 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 -> cvgn u -> M%:E < limn u ->
  \forall n \near \oo, M%:E <= u n.

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

Lemma eseries_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.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgeyPge` or a variant instead")]
Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgeNyPle` or a variant instead")]
Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `squeeze_cvge` and generalized")]
Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
Notation ereal_cvgD_pinfty_pinfty := __deprecated__ereal_cvgD_pinfty_pinfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeD` and generalized")]
Notation ereal_cvgD := __deprecated__ereal_cvgD (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeB` and generalized")]
Notation ereal_cvgB := __deprecated__ereal_cvgB (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `is_cvgeD` and generalized")]
Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvge_sub0` and generalized")]
Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0 (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `limeD` and generalized")]
Notation ereal_limD := __deprecated__ereal_limD (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeM` and generalized")]
Notation ereal_cvgM := __deprecated__ereal_cvgM (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvg_nnesum` and generalized")]
Notation ereal_lim_sum := __deprecated__ereal_lim_sum (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvg_abse0P` and generalized")]
Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0 (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvge_ge` instead")]
Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0 (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `lime_ge` and generalized")]
Notation ereal_lim_ge := __deprecated__ereal_lim_ge (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `lime_le` and generalized")]
Notation ereal_lim_le := __deprecated__ereal_lim_le (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeryP` and generalized")]
Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `fine_cvgP` and generalized")]
Notation ereal_cvg_real := __deprecated__ereal_cvg_real (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `ereal_nondecreasing_cvgn`")]
Notation ereal_nondecreasing_cvg := ereal_nondecreasing_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `ereal_nondecreasing_is_cvgn`")]
Notation ereal_nondecreasing_is_cvg := ereal_nondecreasing_is_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `ereal_nonincreasing_cvgn`")]
Notation ereal_nonincreasing_cvg := ereal_nonincreasing_cvgn (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6",
  note="renamed to `ereal_nonincreasing_is_cvgn`")]
Notation ereal_nonincreasing_is_cvg := ereal_nonincreasing_is_cvgn (only parsing).
#[deprecated(since="analysis 0.6.0", note="Use eseries0 instead.")]
Notation nneseries0 := eseries0 (only parsing).
#[deprecated(since="analysis 0.6.0", note="Use eq_eseriesr instead.")]
Notation eq_nneseries := eq_eseriesr (only parsing).
#[deprecated(since="analysis 0.6.0", note="Use eseries_pred0 instead.")]
Notation nneseries_pred0 := eseries_pred0 (only parsing).
#[deprecated(since="analysis 0.6.0", note="Use eseries_mkcond instead.")]
Notation nneseries_mkcond := eseries_mkcond (only parsing).

Section minr_cvg_0.
Local Open Scope ring_scope.
Context {R : realFieldType}.
Implicit Types (u : R^nat) (r : R).

Lemma minr_cvg_0_cvg_0 u r : 0 < r -> (forall k, 0 <= u k) ->
  minr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.

Lemma maxr_cvg_0_cvg_0 u r : r < 0 -> (forall k, u k <= 0) ->
  maxr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.

End minr_cvg_0.

Section mine_cvg_0.
Context {R : realFieldType}.
Local Open Scope ereal_scope.
Implicit Types (u : (\bar R)^nat) (r : R) (x : \bar R).

Lemma mine_cvg_0_cvg_fin_num u x : 0 < x -> (forall k, 0 <= u k) ->
  mine (u n) x @[n --> \oo] --> 0 ->
  \forall n \near \oo, u n \is a fin_num.

Lemma mine_cvg_minr_cvg u r : (0 < r)%R -> (forall k, 0 <= u k) ->
  mine (u n) r%:E @[n --> \oo] --> 0 ->
  minr (fine (u n)) r @[n --> \oo] --> 0%R.

Lemma mine_cvg_0_cvg_0 u x : 0 < x -> (forall k, 0 <= u k) ->
  mine (u n) x @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.

Lemma maxe_cvg_0_cvg_fin_num u x : x < 0 -> (forall k, u k <= 0) ->
  maxe (u n) x @[n --> \oo] --> 0 ->
  \forall n \near \oo, u n \is a fin_num.

Lemma maxe_cvg_maxr_cvg u r : (r < 0)%R -> (forall k, u k <= 0) ->
  maxe (u n) r%:E @[n --> \oo] --> 0 ->
  maxr (fine (u n)) r @[n --> \oo] --> 0%R.

Lemma maxe_cvg_0_cvg_0 u x : x < 0 -> (forall k, u k <= 0) ->
  maxe (u n) x @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.

End mine_cvg_0.

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) ->
  forall m, has_lbound (sdrop u m).

Lemma has_ubound_sdrop u : has_ubound (range u) ->
  forall 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 : cvgn u -> cvgn (sups u).

Lemma is_cvg_infs u : cvgn u -> cvgn (infs u).

Lemma infs_le_sups u n : cvgn u -> infs u n <= sups u n.

Lemma cvg_sups_inf u : has_ubound (range u) -> has_lbound (range u) ->
  sups u @ \oo --> inf (range (sups u)).

Lemma cvg_infs_sup u : has_ubound (range u) -> has_lbound (range u) ->
  infs u @ \oo --> sup (range (infs u)).

Lemma sups_preimage T (D : set T) r (f : (T -> R)^nat) n :
  (forall 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 :
  (forall 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 limn_sup_limn_inf.
Variable R : realType.
Implicit Types (r : R) (u v : R^o^nat).

Definition limn_sup u := limn (sups u).

Definition limn_inf u := limn (infs u).

Lemma limn_infN u : cvgn u -> limn_inf (-%R \o u) = - limn_sup u.

Lemma limn_supE u : bounded_fun u -> limn_sup u = inf (range (sups u)).

Lemma limn_infE u : bounded_fun u -> limn_inf u = sup (range (infs u)).

Lemma limn_inf_sup u : cvgn u -> limn_inf u <= limn_sup u.

Lemma cvg_limn_inf_sup u l : u @ \oo --> l -> (limn_inf u = l) * (limn_sup u = l).

Lemma cvg_limn_infE u : cvgn u -> limn_inf u = limn u.

Lemma cvg_limn_supE u : cvgn u -> limn_sup u = limn u.

Lemma cvg_sups u l : u @ \oo --> l -> sups u @ \oo --> (l : R^o).

Lemma cvg_infs u l : u @ \oo --> l -> infs u @ \oo --> (l : R^o).

Lemma le_limn_supD u v : bounded_fun u -> bounded_fun v ->
  limn_sup (u \+ v) <= limn_sup u + limn_sup v.

Lemma le_limn_infD u v : bounded_fun u -> bounded_fun v ->
  limn_inf u + limn_inf v <= limn_inf (u \+ v).

Lemma limn_supD u v : cvgn u -> cvgn v ->
  limn_sup (u \+ v) = limn_sup u + limn_sup v.

Lemma limn_infD u v : cvgn u -> cvgn v ->
  limn_inf (u \+ v) = limn_inf u + limn_inf v.

End limn_sup_limn_inf.

#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_sup`")]
Notation lim_sup := limn_sup (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_inf`")]
Notation lim_inf := limn_sup (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_infN`")]
Notation lim_infN := limn_infN (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_supE`")]
Notation lim_supE := limn_supE (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_infE`")]
Notation lim_infE := limn_infE (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_inf_sup`")]
Notation lim_inf_le_lim_sup := limn_inf_sup (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvg_limn_infE`")]
Notation cvg_lim_infE := cvg_limn_infE (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvg_limn_supE`")]
Notation cvg_lim_supE := cvg_limn_supE (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `le_limn_supD`")]
Notation le_lim_supD := le_limn_supD (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `le_limn_infD`")]
Notation le_lim_infD := le_limn_infD (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_supD`")]
Notation lim_supD := limn_supD (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_infD`")]
Notation lim_infD := limn_infD (only parsing).

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 @ \oo --> ereal_inf (range (esups u)).

Lemma is_cvg_esups u : cvgn (esups u).

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

Lemma is_cvg_einfs u : cvgn (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 limn_esup_einf.
Context {R : realType}.
Implicit Type (u : (\bar R)^nat).
Local Open Scope ereal_scope.

Definition limn_esup u := limf_esup u \oo.

Definition limn_einf u := - limn_esup (\- u).

Lemma limn_esup_lim u : limn_esup u = limn (esups u).

Lemma limn_einf_lim u : limn_einf u = limn (einfs u).

End limn_esup_einf.

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

Lemma limn_einf_shift u l : l \is a fin_num ->
  limn_einf (fun x => l + u x) = l + limn_einf u.

Lemma limn_esup_le_cvg u l : limn_esup u <= l -> (forall n, l <= u n) ->
  u @ \oo --> l.

Lemma limn_einfN u : limn_einf (-%E \o u) = - limn_esup u.

Lemma limn_esupN u : limn_esup (-%E \o u) = - limn_einf u.

Lemma limn_einf_sup u : limn_einf u <= limn_esup u.

Lemma cvgNy_limn_einf_sup u : u @ \oo --> -oo ->
  (limn_einf u = -oo) * (limn_esup u = -oo).

Lemma cvgNy_einfs u : u @ \oo --> -oo -> einfs u @ \oo --> -oo.

Lemma cvgNy_esups u : u @ \oo --> -oo -> esups u @ \oo --> -oo.

Lemma cvgy_einfs u : u @ \oo --> +oo -> einfs u @ \oo --> +oo.

Lemma cvgy_esups u : u @ \oo --> +oo -> esups u @ \oo --> +oo.

Lemma cvg_esups u l : u @ \oo --> l -> esups u @ \oo --> l.

Lemma cvg_einfs u l : u @ \oo --> l -> einfs u @ \oo --> l.

Lemma cvg_limn_einf_sup u l : u @ \oo --> l ->
  (limn_einf u = l) * (limn_esup u = l).

Lemma is_cvg_limn_einfE u : cvgn u -> limn_einf u = limn u.

Lemma is_cvg_limn_esupE u : cvgn u -> limn_esup u = limn u.

End lim_esup_inf.
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_einf_shift`")]
Notation lim_einf_shift := limn_einf_shift (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_esup_le_cvg`")]
Notation lim_esup_le_cvg := limn_esup_le_cvg (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_einfN`")]
Notation lim_einfN := limn_einfN (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_esupN`")]
Notation lim_esupN := limn_esupN (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `limn_einf_sup`")]
Notation lim_einf_sup := limn_einf_sup (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvgNy_limn_einf_sup`")]
Notation cvgNy_lim_einf_sup := cvgNy_limn_einf_sup (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `cvg_limn_einf_sup`")]
Notation cvg_lim_einf_sup := cvg_limn_einf_sup (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `is_cvg_limn_einfE`")]
Notation is_cvg_lim_einfE := is_cvg_limn_einfE (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.6", note="renamed to `is_cvg_limn_esupE`")]
Notation is_cvg_lim_esupE := is_cvg_limn_esupE (only parsing).

Lemma geometric_le_lim {R : realType} (n : nat) (a x : R) :
  0 <= a -> 0 < x -> `|x| < 1 -> series (geometric a x) n <= a * (1 - x)^-1.

Section banach_contraction.

Context {R : realType} {X : completeNormedModType R} (U : set X).
Variables (f : {fun U >-> U}).

Section contractions.
Variables (q : {nonneg R}) (ctrf : contraction q f) (base : X) (Ubase : U base).
Let C := `|f base - base| / (1 - q%:num).
Let y := fun n => iter n f base.
Let q1 := ctrf.1.
Let ctrfq := ctrf.2.
Let C_ge0 : 0 <= C.

Lemma contraction_dist n m : `|y n - y (n + m)| <= C * q%:num ^+ n.

Lemma contraction_cvg : cvgn y.

Lemma contraction_cvg_fixed : closed U -> limn y = f (limn y).

End contractions.

Variable ctrf : is_contraction f.

Theorem banach_fixed_point : closed U -> U !=set0 -> exists2 p, U p & p = f p.

End banach_contraction.