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.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import set_interval.
Require Import reals ereal signed 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: 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 (resp. non- positive) extended numbers use the string "nneseries" (resp. "npeseries") 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 lim_e{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.

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.
#[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 →
  ∀ 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 __deprecated__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.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `squeeze_cvgr`")]
Notation squeeze := __deprecated__squeeze.

Lemma __deprecated__cvgPpinfty (u_ : R ^nat) :
  u_ --> +oo ↔ ∀ A, \∀ 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.

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

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

Lemma __deprecated__cvgPninfty (u_ : R ^nat) :
  u_ --> -oo ↔ ∀ A, \∀ 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.

Lemma __deprecated__ger_cvg_pinfty u_ v_ : (\∀ n \near \oo , u_ n ≤ v_ n ) →
  u_ --> +oo → v_ --> +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.

Lemma __deprecated__ler_cvg_ninfty v_ u_ : (\∀ n \near \oo , u_ n ≤ v_ n ) →
  v_ --> -oo → u_ --> -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.

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

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

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

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

Lemma __deprecated__cvgPpinfty_lt (u_ : R ^nat) :
  u_ --> +oo%R ↔ ∀ A, \∀ 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.

Lemma __deprecated__cvgPninfty_lt (u_ : R ^nat) :
  u_ --> -oo%R ↔ ∀ A, \∀ 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.

Lemma __deprecated__cvgPpinfty_near (u_ : R ^nat) :
  u_ --> +oo%R ↔ \∀ A \near +oo , \∀ 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.

Lemma __deprecated__cvgPninfty_near (u_ : R ^nat) :
  u_ --> -oo%R ↔ \∀ A \near -oo , \∀ 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.

Lemma __deprecated__cvgPpinfty_lt_near (u_ : R ^nat) :
  u_ --> +oo%R ↔ \∀ A \near +oo , \∀ 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.

Lemma __deprecated__cvgPninfty_lt_near (u_ : R ^nat) :
  u_ --> -oo%R ↔ \∀ A \near -oo , \∀ 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.

End sequences_R_lemmas_realFieldType.

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

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

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 cvge_harmonic {R : archiFieldType} : (EFin \o @harmonic R ) @ \oo --> 0%E.

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 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 --> (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 __deprecated__nat_dvg_real (R : realType) (u_ : nat ^nat) : u_ --> \oo →
  ([sequence (u_ n)%:R : R^o]_n --> +oo)%R.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgrnyP` and generalized")]
Notation nat_dvg_real := __deprecated__nat_dvg_real.

Lemma __deprecated__nat_cvgPpinfty (u : nat ^nat) :
  u --> \oo ↔ ∀ A, \∀ 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.

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 __deprecated__ereal_cvg_abs0 (R : realFieldType) (f : (\bar R )^nat) :
  abse \o f --> nbhs 0 → f --> 0.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvg_abse0P` and generalized")]
Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0.

Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R )^nat) (a : \bar R) :
  (∀ n, 0 ≤ f n ) → f --> a → 0 ≤ a.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvge_ge` instead")]
Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0.

Lemma __deprecated__ereal_lim_ge (R : realFieldType) x (u_ : (\bar R )^nat) : cvg u_ →
  (\∀ n \near \oo , x ≤ u_ n ) → x ≤ lim u_.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `lime_ge` and generalized")]
Notation ereal_lim_ge := __deprecated__ereal_lim_ge.

Lemma __deprecated__ereal_lim_le (R : realFieldType) x (u_ : (\bar R )^nat) : cvg u_ →
  (\∀ n \near \oo , u_ n ≤ x ) → lim u_ ≤ x.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `lime_le` and generalized")]
Notation ereal_lim_le := __deprecated__ereal_lim_le.

Lemma __deprecated__dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) :
  u_ --> +oo%R → [sequence (u_ n )%:E ]_n --> +oo.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeryP` and generalized")]
Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg.

Lemma __deprecated__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.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `fine_cvgP` and generalized")]
Notation ereal_cvg_real := __deprecated__ereal_cvg_real.

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

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

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 eseries_cond {R : numFieldType} (f : nat → \bar R) 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 : nat → \bar R) 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 : nat → \bar R) 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} :
  (∀ 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 : (∀ 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 :
  (∀ 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 : (∀ 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 :
  (∀ n, (m ≤ n)%N → P n → 0 ≤ u_ n ) →
cvg (fun n ⇒ \sum_(m ≤ i < n | P i ) u_ i).

Lemma is_cvg_ereal_npos_natsum_cond m P :
  (∀ n, (m ≤ n)%N → P n → u_ n ≤ 0) →
  cvg (fun n ⇒ \sum_(m ≤ i < n | P i ) u_ i).

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

Lemma is_cvg_ereal_npos_natsum m : (∀ n, (m ≤ n)%N → u_ n ≤ 0) →
  cvg (fun n ⇒ \sum_(m ≤ i < n ) u_ i).

Lemma is_cvg_nneseries_cond P N : (∀ n, P n → 0 ≤ u_ n ) →
  cvg (fun n ⇒ \sum_(N ≤ i < n | P i ) u_ i).

Lemma is_cvg_npeseries_cond P N : (∀ n, P n → u_ n ≤ 0) →
  cvg (fun n ⇒ \sum_(N ≤ i < n | P i ) u_ i).

Lemma is_cvg_nneseries P N : (∀ n, P n → 0 ≤ u_ n ) →
  cvg (fun n ⇒ \sum_(N ≤ i < n | P i ) u_ i).

Lemma is_cvg_npeseries P N : (∀ n, P n → u_ n ≤ 0) →
  cvg (fun n ⇒ \sum_(N ≤ i < n | P i ) u_ i).

Lemma nneseries_ge0 P N : (∀ n, P n → 0 ≤ u_ n ) →
  0 ≤ \sum_(N ≤ i <oo | P i ) u_ i.

Lemma npeseries_le0 P N : (∀ 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) :
  (∀ i, 0 ≤ u i)%R → \sum_(k <oo ) (u k )%:E < +oo → cvg (series u).

Lemma nneseriesZl (R : realType) (f : nat → \bar R) (P : pred nat) x N :
  (∀ 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) :
  (∀ 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 __deprecated__ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R )^nat) :
  u_ --> +oo ↔ (∀ A, (0 < A)%R → \∀ n \near \oo , A %:E ≤ u_ n ).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgeyPge` or a variant instead")]
Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty.

Lemma __deprecated__ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R )^nat) :
  u_ --> -oo ↔ (∀ A, (A < 0)%R → \∀ n \near \oo , u_ n ≤ A %:E ).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use `cvgeNyPle` or a variant instead")]
Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty.

Lemma __deprecated__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.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `squeeze_cvge` and generalized")]
Notation ereal_squeeze := __deprecated__ereal_squeeze.

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 lee_nneseries (R : realType) (u v : (\bar R )^nat) (P : pred nat) N :
  (∀ i, P i → 0 ≤ u i ) →
  (∀ 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) :
  (∀ i, P i → u i ≤ 0) → (∀ 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 → g --> b %:E → f \+ g --> +oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin.

Lemma __deprecated__ereal_cvgD_ninfty_fin (R : realFieldType) (f g : (\bar R )^nat) b :
  f --> -oo → g --> b %:E → f \+ g --> -oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin.

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

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

Lemma __deprecated__ereal_cvgD (R : realFieldType) (f g : (\bar R )^nat) a b :
  a +? b → f --> a → g --> b → f \+ g --> a + b.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeD` and generalized")]
Notation ereal_cvgD := __deprecated__ereal_cvgD.

Section nneseries_split.

Lemma __deprecated__ereal_cvgB (R : realFieldType) (f g : (\bar R )^nat) a b :
  a +? - b → f --> a → g --> b → f \- g --> a - b.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeB` and generalized")]
Notation ereal_cvgB := __deprecated__ereal_cvgB.

Lemma __deprecated__ereal_is_cvgD (R : realFieldType) (u v : (\bar R )^nat) :
  lim u +? lim v → cvg u → cvg v → cvg (u \+ v).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `is_cvgeD` and generalized")]
Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD.

Lemma __deprecated__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.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvge_sub0` and generalized")]
Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0.

Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R )^nat) :
  cvg f → cvg g → lim f +? lim g →
  lim (f \+ g) = lim f + lim g.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `limeD` and generalized")]
Notation ereal_limD := __deprecated__ereal_limD.

Lemma __deprecated__ereal_cvgM_gt0_pinfty (R : realFieldType) (f g : (\bar R )^nat) b :
  (0 < b)%R → f --> +oo → g --> b %:E → f \* g --> +oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty.

Lemma __deprecated__ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R )^nat) b :
  (b < 0)%R → f --> +oo → g --> b %:E → f \* g --> -oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty.

Lemma __deprecated__ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R )^nat) b :
  (0 < b)%R → f --> -oo → g --> b %:E → f \* g --> -oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty.

Lemma __deprecated__ereal_cvgM_lt0_ninfty (R : realFieldType) (f g : (\bar R )^nat) b :
  (b < 0)%R → f --> -oo → g --> b %:E → f \* g --> +oo.
#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty.

Lemma __deprecated__ereal_cvgM (R : realType) (f g : (\bar R ) ^nat) (a b : \bar R) :
a *? b → f --> a → g --> b → f \* g --> a × b.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvgeM` and generalized")]
Notation ereal_cvgM := __deprecated__ereal_cvgM.

Lemma __deprecated__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.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed to `cvg_nnesum` and generalized")]
Notation ereal_lim_sum := __deprecated__ereal_lim_sum.

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 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 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 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="analysis 0.6.0", note="Use eseries0 instead.")]
Notation nneseries0 := eseries0.
#[deprecated(since="analysis 0.6.0", note="Use eq_eseriesr instead.")]
Notation eq_nneseries := eq_eseriesr.
#[deprecated(since="analysis 0.6.0", note="Use eseries_pred0 instead.")]
Notation nneseries_pred0 := eseries_pred0.
#[deprecated(since="analysis 0.6.0", note="Use eseries_mkcond instead.")]
Notation nneseries_mkcond := eseries_mkcond.

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.

Module LimSup.
Definition lim_esup (R : realType) (u : (\bar R )^nat) := lim (esups u).
Definition lim_einf (R : realType) (u : (\bar R )^nat) := lim (einfs u).
End LimSup.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_esup`")]
Notation elim_sup := LimSup.lim_esup.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_einf`")]
Notation elim_inf := LimSup.lim_einf.

Notation lim_esup := LimSup.lim_esup.
Notation lim_einf := LimSup.lim_einf.

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

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

Lemma lim_esup_le_cvg u l : lim_esup u ≤ l → (∀ n, l ≤ u n ) → u --> l.

Lemma lim_einfN u : lim_einf (-%E \o u) = - lim_esup u.

Lemma lim_esupN u : lim_esup (-%E \o u) = - lim_einf u.

Lemma lim_einf_sup u : lim_einf u ≤ lim_esup u.

Lemma cvgNy_lim_einf_sup u : u --> -oo →
  (lim_einf u = -oo ) × (lim_esup u = -oo ).

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

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

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

Lemma cvgy_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_lim_einf_sup u l : u --> l → (lim_einf u = l ) × (lim_esup u = l ).

Lemma is_cvg_lim_einfE u : cvg u → lim_einf u = lim u.

Lemma is_cvg_lim_esupE u : cvg u → lim_esup u = lim u.

End lim_esup_inf.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_einf_shift`")]
Notation elim_inf_shift := lim_einf_shift.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_esup_le_cvg`")]
Notation elim_sup_le_cvg := lim_esup_le_cvg.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_einfN`")]
Notation elim_infN := lim_einfN.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_esupN`")]
Notation elim_supN := lim_esupN.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `lim_einf_sup`")]
Notation elim_inf_sup := lim_einf_sup.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgNy_lim_einf_sup`")]
Notation cvg_ninfty_elim_inf_sup := cvgNy_lim_einf_sup.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgNy_einfs`")]
Notation cvg_ninfty_einfs := cvgNy_einfs.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgNy_esups`")]
Notation cvg_ninfty_esups := cvgNy_esups.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgy_einfs`")]
Notation cvg_pinfty_einfs := cvgy_einfs.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgy_esups`")]
Notation cvg_pinfty_esups := cvgy_esups.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim_einf_sup`")]
Notation cvg_elim_inf_sup := cvg_lim_einf_sup.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `is_cvg_lim_einfE`")]
Notation is_cvg_elim_infE := is_cvg_lim_einfE.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `is_cvg_lim_esupE`")]
Notation is_cvg_elim_supE := is_cvg_lim_esupE.

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 : cvg y.

Lemma contraction_cvg_fixed : closed U → lim y = f (lim 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.