Library mathcomp.analysis.sequences

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

Definitions and lemmas about sequences

The purpose of this file is to gather generic definitions and lemmas about sequences. The first part is essentially about sequences of realType numbers while the last part is about extended real numbers. It is an early version that is likely to undergo changes. The documentation lists up sample definitions and lemmas to give an idea of contents.

Definitions: R ^nat == notation for sequences, i.e., functions of type nat -> R harmonic == harmonic sequence arithmetic == arithmetic sequence geometric == geometric sequence series u == the sequence of partial sums of u [sequence u_n]_n == the sequence of general element u_n [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])

Lemmas: squeeze == squeeze lemma cvgNpinfty u == (- u --> +oo) = (u --> -oo). nonincreasing_cvg_ge u == if u is nonincreasing and convergent then forall n, lim u <= u n nondecreasing_cvg_le u == if u is nondecreasing and convergent then forall n, lim u >= u n nondecreasing_cvg u == if u is nondecreasing and bounded then u is convergent and its limit is sup u_n nonincreasing_cvg u == if u is nonincreasing u and bound by below then u is convergent adjacent == adjacent sequences lemma cesaro == Cesaro's lemma

Sections sequences_R* contain properties of sequences of real numbers.

is_cvg_series_exp_coeff == convergence of \sum_n^+oo x^n / n! expR x == the exponential function defined on a realType

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

Section sequences_ereal contain properties of sequences of extended real numbers.

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 ident, format "[ 'sequence' E ]_ n").
Reserved Notation "[ 'series' E ]_ n"
  (at level 0, E at level 0, n ident, 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)) : 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 ??

Section sequences_patched.

TODO: generalizations to numDomainType

Section NatShift.

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

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

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

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

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

End NatShift.

Variables (V : topologicalType).

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

End sequences_patched.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

End sequences_R_lemmas_realFieldType.

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

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

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

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

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

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

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

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

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

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

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

End partial_sum.

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

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

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

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

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

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

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

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

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

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

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

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

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

End partial_sum_numFieldType.

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

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

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

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

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

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

End series_patched.

Section sequences_R_lemmas.
Variable R : realType.

Lemma nondecreasing_cvg (u_ : R ^nat) :
    nondecreasing_seq u_ → has_ubound [set of u_] →
  u_ --> sup [set of u_].

Lemma nondecreasing_is_cvg (u_ : R ^nat) :
  nondecreasing_seq u_ → has_ubound [set of 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 [set of u_] →
  u_ --> inf (u_ @` setT).

Lemma nonincreasing_is_cvg (u_ : R ^nat) :
  nonincreasing_seq u_ → has_lbound [set of u_] → cvg u_.

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

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

End sequences_R_lemmas.

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

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

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

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

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

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

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

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

Section cesaro.
Variable R : archiFieldType.

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

End cesaro.

Section cesaro_converse.
Variable R : archiFieldType.

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

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

End cesaro_converse.

Section series_convergence.

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

Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) :
  (∀ n, 0 ≤ u_ n ) → nondecreasing_seq (series u_).

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

End series_convergence.

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

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

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

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

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

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

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

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

Lemma cvg_geometric (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.

TODO: backport to MathComp?

Section fact_facts.

Local Open Scope nat_scope.

Lemma leq_fact n : n ≤ n`!.

Lemma prod_rev n m :
  \prod_(0 ≤ k < n - m) (n - k) = \prod_(m.+1 ≤ k < n.+1) k.

Lemma fact_split n m : m ≤ n → n`! = \prod_(0 ≤ k < n - m) (n - k) × m`!.

End fact_facts.

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 [set of 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 [set of S1 N ] (sup [set of S0 N ]).

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

End exponential_series_cvg.

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

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

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

End exponential_series.

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

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

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

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

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

End sequences_ereal_realDomainType.

Section sequences_ereal.
Local Open Scope ereal_scope.

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

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

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

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

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

Lemma dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) :
  u_ --> +oo%R → (fun n ⇒ (u_ n )%:E ) --> +oo.

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

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

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

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

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

NB: see also nondecreasing_series