Module mathcomp.analysis.sequences
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.From mathcomp Require Import interval rat archimedean.
From mathcomp Require Import 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.
nondecreasing_seq u == the sequence u is non-decreasing
nonincreasing_seq u == the sequence u is non-increasing
increasing_seq u == the sequence u is (strictly) increasing
decreasing_seq u == the sequence u is (strictly) decreasing
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_cvgn_ge u_ == if u_ is nonincreasing and convergent then
forall n, lim u_ <= u_ n
nondecreasing_cvgn_le u_ == if u_ is nondecreasing and convergent then
forall n, lim u_ >= u_ n
nondecreasing_cvgn u_ == if u_ is nondecreasing and bounded then u_
is convergent and its limit is sup u_n
nonincreasing_cvgn 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 for sequences:
sdrop u n := {u_k | k >= n}
sups u := [sequence sup (sdrop u n)]_n
infs u := [sequence inf (sdrop u n)]_n
limn_sup, limn_inf == limit sup/inferior for a sequence of reals
esups u := [sequence ereal_sup (sdrop u n)]_n
einfs u := [sequence ereal_inf (sdrop u n)]_n
limn_esup u, limn_einf == limit sup/inferior for a sequence of
of extended reals
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.
From mathcomp Require Import mathcomp_extra.
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_.
Proof.
Lemma nonincreasing_opp (T : numDomainType) (u_ : T ^nat) :
nonincreasing_seq (- u_) = nondecreasing_seq u_.
Proof.
Lemma decreasing_opp (T : numDomainType) (u_ : T ^nat) :
decreasing_seq (- u_) = increasing_seq u_.
Proof.
Lemma increasing_opp (T : numDomainType) (u_ : T ^nat) :
increasing_seq (- u_) = decreasing_seq u_.
Proof.
Lemma nondecreasing_seqP d (T : porderType d) (u_ : T ^nat) :
(forall n, u_ n <= u_ n.+1)%O <-> nondecreasing_seq u_.
Proof.
Lemma nonincreasing_seqP d (T : porderType d) (u_ : T ^nat) :
(forall n, u_ n >= u_ n.+1)%O <-> nonincreasing_seq u_.
Proof.
Lemma increasing_seqP d (T : porderType d) (u_ : T ^nat) :
(forall n, u_ n < u_ n.+1)%O <-> increasing_seq u_.
Proof.
Lemma decreasing_seqP d (T : porderType d) (u_ : T ^nat) :
(forall n, u_ n > u_ n.+1)%O <-> decreasing_seq u_.
Proof.
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}.
Proof.
Lemma nondecreasing_seqD T (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)).
Proof.
Local Notation eqolimn := (@eqolim _ _ _ eventually_filter).
Local Notation eqolimPn := (@eqolimP _ _ _ eventually_filter).
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).
Proof.
Lemma bigsetU_seqDU F n :
\big[setU/set0]_(k < n) F k = \big[setU/set0]_(k < n) seqDU F k.
Proof.
Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k.
Proof.
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).
Proof.
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.
Proof.
Lemma trivIset_seqD F : nondecreasing_seq F -> trivIset setT (seqD F).
Proof.
Lemma bigsetU_seqD F n :
\big[setU/set0]_(i < n) F i = \big[setU/set0]_(i < n) seqD F i.
Proof.
Lemma setU_seqD F : nondecreasing_seq F ->
forall n, F n.+1 = F n `|` seqD F n.+1.
Proof.
Lemma nondecreasing_bigsetU_seqD F n : nondecreasing_seq F ->
\big[setU/set0]_(i < n.+1) seqD F i = F n.
Proof.
Lemma eq_bigcup_seqD F : \bigcup_n seqD F n = \bigcup_n F n.
Proof.
Lemma eq_bigcup_seqD_bigsetU F :
\bigcup_n (seqD (fun n => \big[setU/set0]_(i < n.+1) F i) n) = \bigcup_n F n.
Proof.
Lemma bigcup_bigsetU_bigcup F :
\bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k.
Proof.
End seqD.
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed to `nondecreasing_bigsetU_seqD`")]
Notation eq_bigsetU_seqD := nondecreasing_bigsetU_seqD (only parsing).
Convergence of patched sequences
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).
Proof.
Lemma is_cvg_restrict f u_ :
cvgn [sequence if (n <= N)%nat then f n else u_ n]_n = cvgn u_.
Proof.
Lemma cvg_centern u_ l :
([sequence u_ (n - N)%N]_n @ \oo --> l) = (u_ @ \oo --> l).
Proof.
Lemma cvg_shiftn u_ l :
([sequence u_ (n + N)%N]_n @ \oo --> l) = (u_ @ \oo --> l).
Proof.
End NatShift.
Variables (V : topologicalType).
Lemma cvg_shiftS u_ (l : V) :
([sequence u_ n.+1]_n @ \oo --> l) = (u_ @ \oo --> l).
Proof.
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.
Proof.
#[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.
Proof.
#[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).
Proof.
#[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).
Proof.
#[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.
Proof.
#[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.
Proof.
#[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.
Proof.
#[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).
Proof.
#[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).
Proof.
#[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.
Proof.
Lemma nonincreasing_cvgn_ge u_ : nonincreasing_seq u_ -> cvgn u_ ->
forall n, limn u_ <= u_ n.
Proof.
Lemma nondecreasing_cvgn_le u_ : nondecreasing_seq u_ -> cvgn u_ ->
forall n, u_ n <= limn u_.
Proof.
Lemma cvg_has_ub u_ : cvgn u_ -> has_ubound [set `|u_ n| | n in setT].
Proof.
Lemma cvg_has_sup u_ : cvgn u_ -> has_sup (u_ @` setT).
Proof.
Lemma cvg_has_inf u_ : cvgn u_ -> has_inf (u_ @` setT).
Proof.
Lemma __deprecated__cvgPpinfty_lt (u_ : R ^nat) :
u_ @ \oo --> +oo%R <-> forall A, \forall n \near \oo, (A < u_ n)%R.
Proof.
#[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.
Proof.
#[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.
Proof.
#[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.
Proof.
#[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.
Proof.
#[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.
Proof.
#[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).
Proof.
#[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).
Proof.
#[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.
Proof.
Lemma seriesEord : series = [sequence \sum_(k < n) u_ k]_n.
Proof.
Lemma seriesSr n : series n.+1 = series n + u_ n.
Proof.
Lemma seriesS n : series n.+1 = u_ n + series n.
Proof.
Lemma seriesSB (n : nat) : series n.+1 - series n = u_ n.
Proof.
Lemma series_addn m n : series (n + m)%N = series m + \sum_(m <= k < n + m) u_ k.
Proof.
Lemma sub_series_geq m n : (m <= n)%N ->
series n - series m = \sum_(m <= k < n) u_ k.
Proof.
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.
Proof.
Lemma sub_double_series n : series n.*2 - series n = \sum_(n <= k < n.*2) u_ k.
Proof.
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.
Proof.
Lemma seriesD (V : zmodType) (f g : V ^nat) : series (f + g) = series f + series g.
Proof.
Lemma seriesZ (R : ringType) (V : lmodType R) (f : V ^nat) k :
series (k *: f) = k *: series f.
Proof.
Section partial_sum_numFieldType.
Variables V : numFieldType.
Implicit Types f g : V ^nat.
Lemma is_cvg_seriesN f : cvgn (series (- f)) = cvgn (series f).
Proof.
Lemma lim_seriesN f : cvg (series f @ \oo) ->
limn (series (- f)) = - limn (series f).
Proof.
Lemma is_cvg_seriesZ f k : cvgn (series f) -> cvgn (series (k *: f)).
Proof.
Lemma lim_seriesZ f k : cvgn (series f) ->
limn (series (k *: f)) = k *: limn (series f).
Proof.
Lemma is_cvg_seriesD f g :
cvgn (series f) -> cvgn (series g) -> cvgn (series (f + g)).
Proof.
Lemma lim_seriesD f g : cvgn (series f) -> cvgn (series g) ->
limn (series (f + g)) = limn (series f) + limn (series g).
Proof.
Lemma is_cvg_seriesB f g :
cvgn (series f) -> cvgn (series g) -> cvgn (series (f - g)).
Proof.
Lemma lim_seriesB f g : cvg (series f @ \oo) -> cvg (series g @ \oo) ->
limn (series (f - g)) = limn (series f) - limn (series g).
Proof.
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).
Proof.
Lemma telescopeK (V : zmodType) (u_ : V ^nat) :
series (telescope u_) = [sequence u_ n - u_ 0%N]_n.
Proof.
Lemma seriesK (V : zmodType) : cancel (@series V) telescope.
Proof.
Lemma eq_sum_telescope (V : zmodType) (u_ : V ^nat) n :
u_ n = u_ 0%N + series (telescope u_) n.
Proof.
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_).
Proof.
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_).
Proof.
Lemma nondecreasing_is_cvgn (u_ : R ^nat) :
nondecreasing_seq u_ -> has_ubound (range u_) -> cvgn u_.
Proof.
Lemma nondecreasing_dvgn_lt (u_ : R ^nat) :
nondecreasing_seq u_ -> ~ cvgn u_ -> u_ @ \oo --> +oo.
Proof.
Lemma near_nondecreasing_is_cvgn (u_ : R ^nat) (M : R) :
{near \oo, nondecreasing_seq u_} -> (\forall n \near \oo, u_ n <= M) ->
cvgn u_.
Proof.
Lemma nonincreasing_cvgn (u_ : R ^nat) :
nonincreasing_seq u_ -> has_lbound (range u_) ->
u_ @ \oo --> inf (u_ @` setT).
Proof.
Lemma nonincreasing_is_cvgn (u_ : R ^nat) :
nonincreasing_seq u_ -> has_lbound (range u_) -> cvgn u_.
Proof.
Lemma near_nonincreasing_is_cvgn (u_ : R ^nat) (m : R) :
{near \oo, nonincreasing_seq u_} -> (\forall n \near \oo, m <= u_ n) ->
cvgn u_.
Proof.
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_].
Proof.
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.
Proof.
Lemma harmonic_ge0 {R : numFieldType} i : 0 <= harmonic i :> R.
Proof.
Lemma cvg_harmonic {R : archiFieldType} : @harmonic R @ \oo --> 0.
Proof.
Lemma cvge_harmonic {R : archiFieldType} : (EFin \o @harmonic R) @ \oo --> 0%E.
Proof.
Lemma dvg_harmonic (R : numFieldType) : ~ cvgn (series (@harmonic R)).
Proof.
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.
Proof.
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).
Proof.
Lemma cesaro_converse (u_ : R ^nat) (l : R) :
telescope u_ =o_\oo @harmonic R ->
arithmetic_mean u_ @ \oo --> l -> u_ @ \oo --> l.
Proof.
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).
Proof.
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.
Proof.
Lemma increasing_series (R : numFieldType) (u_ : R ^nat) :
(forall n, 0 < u_ n) -> increasing_seq (series u_).
Proof.
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.
Proof.
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.
Proof.
Lemma cvg_arithmetic (R : archiFieldType) a (z : R) :
z > 0 -> arithmetic a z @ \oo --> +oo.
Proof.
Lemma cvg_expr (R : archiFieldType) (z : R) :
`|z| < 1 -> (GRing.exp z : R ^nat) @ \oo --> (0 : R).
Proof.
Lemma geometric_seriesE (R : numFieldType) (a z : R) : z != 1 ->
series (geometric a z) = [sequence a * (1 - z ^+ n) / (1 - z)]_n.
Proof.
Lemma cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 ->
series (geometric a z) @ \oo --> (a * (1 - z)^-1).
Proof.
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).
Proof.
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.
Proof.
Lemma cvg_geometric (R : archiFieldType) (a z : R) : `|z| < 1 ->
geometric a z @ \oo --> (0 : R).
Proof.
Lemma is_cvg_geometric_series (R : archiFieldType) (a z : R) : `|z| < 1 ->
cvgn (series (geometric a z)).
Proof.
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_.
Proof.
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.
Proof.
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_).
Proof.
Lemma normed_cvg {R : realType} (V : completeNormedModType R) (u_ : V ^nat) :
cvgn [normed series u_] -> cvgn (series u_).
Proof.
Lemma lim_series_norm {R : realType} (V : completeNormedModType R) (f : V ^nat) :
cvgn [normed series f] ->
`|limn (series f)| <= limn [normed series f].
Proof.
Section series_linear.
Lemma cvg_series_bounded (R : realFieldType) (f : R ^nat) :
cvgn (series f) -> bounded_fun f.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma series_exp_coeff0 n : series (exp 0) n.+1 = 1.
Proof.
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).
Proof.
Let S0_ge0 N n : 0 <= S0 N n.
Proof.
Let S0_sup N n : x < N%:R -> S0 N n <= sup (range (S0 N)).
Proof.
Let S1 N n := \sum_(N.+1 <= i < n) exp x i.
Lemma incr_S1 N : nondecreasing_seq (S1 N).
Proof.
Let S1_sup N : x < N%:R -> ubound (range (S1 N)) (sup (range (S0 N))).
Proof.
Lemma is_cvg_series_exp_coeff_pos : cvgn (series (exp x)).
Proof.
End exponential_series_cvg.
Lemma normed_series_exp_coeff x : [normed series (exp x)] = series (exp `|x|).
Proof.
Lemma is_cvg_series_exp_coeff x : cvgn (series (exp x)).
Proof.
Lemma cvg_exp_coeff x : exp x @ \oo --> (0 : R).
Proof.
End exponential_series.
Definition expR {R : realType} (x : R) : R := limn (series (exp_coeff x)).
Sequences of natural numbers
Lemma __deprecated__nat_dvg_real (R : realType) (u_ : nat ^nat) :
u_ @ \oo --> \oo -> ([sequence (u_ n)%:R : R^o]_n @ \oo --> +oo)%R.
Proof.
#[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.
Proof.
#[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_.
Proof.
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.
Proof.
Lemma cvg_nseries_near (u : nat^nat) : cvgn (nseries u) ->
\forall n \near \oo, u n = 0%N.
Proof.
Lemma dvg_nseries (u : nat^nat) : ~ cvgn (nseries u) ->
nseries u @ \oo --> \oo.
Proof.
Sequences of extended real numbers
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.
Proof.
Lemma eseriesEord : eseries = [sequence \sum_(k < n) u_ k]_n.
Proof.
Lemma eseriesSr n : eseries n.+1 = eseries n + u_ n.
Proof.
Lemma eseriesS n : eseries n.+1 = u_ n + eseries n.
Proof.
Lemma eseriesSB (n : nat) :
eseries n \is a fin_num -> eseries n.+1 - eseries n = u_ n.
Proof.
Lemma eseries_addn m n : eseries (n + m)%N = eseries m + \sum_(m <= k < n + m) u_ k.
Proof.
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.
Proof.
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.
Proof.
Lemma sub_double_eseries n : eseries n \is a fin_num ->
eseries n.*2 - eseries n = \sum_(n <= k < n.*2) u_ k.
Proof.
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.
Proof.
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_.
Proof.
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.
Proof.
Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) :
(forall n, 0 <= f n) -> f @ \oo --> a -> 0 <= a.
Proof.
Lemma __deprecated__ereal_lim_ge (R : realFieldType) x (u_ : (\bar R)^nat) :
cvgn u_ -> (\forall n \near \oo, x <= u_ n) -> x <= limn u_.
Proof.
Lemma __deprecated__ereal_lim_le (R : realFieldType) x (u_ : (\bar R)^nat) :
cvgn u_ -> (\forall n \near \oo, u_ n <= x) -> limn u_ <= x.
Proof.
Lemma __deprecated__dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) :
u_ @ \oo --> +oo%R -> [sequence (u_ n)%:E]_n @ \oo --> +oo.
Proof.
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.
Proof.
Lemma ereal_nondecreasing_cvgn (R : realType) (u_ : (\bar R)^nat) :
nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (range u_).
Proof.
Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
nondecreasing_seq u_ -> cvgn u_.
Proof.
Lemma ereal_nonincreasing_cvgn (R : realType) (u_ : (\bar R)^nat) :
nonincreasing_seq u_ -> u_ @ \oo --> ereal_inf (u_ @` setT).
Proof.
Lemma ereal_nonincreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
nonincreasing_seq u_ -> cvgn u_.
Proof.
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).
Proof.
Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) :
f = g -> limn f = limn g.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Arguments eq_eseriesl {R P} Q.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.
Proof.
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.
Proof.
Lemma ereal_series k : \sum_(k <= i <oo) f i = \sum_(i <oo | (k <= i)%N) f i.
Proof.
Lemma eseries0 N P : (forall i, (N <= i)%N -> P i -> f i = 0) ->
\sum_(N <= i <oo | P i) f i = 0.
Proof.
Lemma eseries_pred0 P : P =1 xpred0 -> \sum_(i <oo | P i) f i = 0.
Proof.
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.
Proof.
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.
Proof.
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).
Proof.
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).
Proof.
Lemma is_cvg_ereal_nneg_natsum m : (forall n, (m <= n)%N -> 0 <= u_ n) ->
cvgn (fun n => \sum_(m <= i < n) u_ i).
Proof.
Lemma is_cvg_ereal_npos_natsum m : (forall n, (m <= n)%N -> u_ n <= 0) ->
cvgn (fun n => \sum_(m <= i < n) u_ i).
Proof.
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).
Proof.
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).
Proof.
Lemma is_cvg_nneseries P N : (forall n, P n -> 0 <= u_ n) ->
cvgn (fun n => \sum_(N <= i < n | P i) u_ i).
Proof.
Lemma is_cvg_npeseries P N : (forall n, P n -> u_ n <= 0) ->
cvgn (fun n => \sum_(N <= i < n | P i) u_ i).
Proof.
Lemma nneseries_ge0 P N : (forall n, P n -> 0 <= u_ n) ->
0 <= \sum_(N <= i <oo | P i) u_ i.
Proof.
Lemma npeseries_le0 P N : (forall n : nat, P n -> u_ n <= 0) ->
\sum_(N <= i <oo | P i) u_ i <= 0.
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma __deprecated__ereal_cvgD_pinfty_pinfty (R : realFieldType) (f g : (\bar R)^nat) :
f @ \oo --> +oo -> g @ \oo --> +oo -> f \+ g @ \oo --> +oo.
Proof.
Lemma __deprecated__ereal_cvgD_ninfty_ninfty (R : realFieldType) (f g : (\bar R)^nat) :
f @ \oo --> -oo -> g @ \oo --> -oo -> f \+ g @ \oo --> -oo.
Proof.
#[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.
Proof.
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.
Proof.
Lemma __deprecated__ereal_is_cvgD (R : realFieldType) (u v : (\bar R)^nat) :
limn u +? limn v -> cvgn u -> cvgn v -> cvgn (u \+ v).
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Lemma nneseries_split (R : realType) (f : nat -> \bar R) N n :
(forall k, (N <= k)%N -> 0 <= f k) ->
\sum_(N <= k <oo) f k = \sum_(N <= k < N + n) f k + \sum_(N + n <= k <oo) f k.
Proof.
End nneseries_split.
Arguments nneseries_split {R f} _ _.
Lemma nneseries_recl (R : realType) (f : nat -> \bar R) :
(forall k, 0 <= f k) -> \sum_(k <oo) f k = f 0%N + \sum_(1 <= k <oo) f k.
Proof.
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.
Proof.
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.
Proof.
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)).
Proof.
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.
Proof.
Lemma nneseries_addn {R : realType} (f : (\bar R)^nat) k :
(forall i, 0 <= f i) ->
\sum_(i <oo) f (i + k)%N = \sum_(k <= i <oo) f i.
Proof.
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.
Proof.
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.
Proof.
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).
Arguments nneseries_split {R f} _ _.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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 : Order.disp_t) (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).
Proof.
Lemma has_ubound_sdrop u : has_ubound (range u) ->
forall m, has_ubound (sdrop u m).
Proof.
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.
Proof.
Lemma infsN u : infs (-%R \o u) = - sups u.
Proof.
Lemma nonincreasing_sups u : has_ubound (range u) ->
nonincreasing_seq (sups u).
Proof.
Lemma nondecreasing_infs u : has_lbound (range u) ->
nondecreasing_seq (infs u).
Proof.
Lemma is_cvg_sups u : cvgn u -> cvgn (sups u).
Proof.
Lemma is_cvg_infs u : cvgn u -> cvgn (infs u).
Proof.
Lemma infs_le_sups u n : cvgn u -> infs u n <= sups u n.
Proof.
Lemma cvg_sups_inf u : has_ubound (range u) -> has_lbound (range u) ->
sups u @ \oo --> inf (range (sups u)).
Proof.
Lemma cvg_infs_sup u : has_ubound (range u) -> has_lbound (range u) ->
infs u @ \oo --> sup (range (infs u)).
Proof.
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[.
Proof.
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[.
Proof.
Lemma bounded_fun_has_lbound_sups u :
bounded_fun u -> has_lbound (range (sups u)).
Proof.
Lemma bounded_fun_has_ubound_infs u :
bounded_fun u -> has_ubound (range (infs u)).
Proof.
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.
Proof.
Lemma limn_supE u : bounded_fun u -> limn_sup u = inf (range (sups u)).
Proof.
Lemma limn_infE u : bounded_fun u -> limn_inf u = sup (range (infs u)).
Proof.
Lemma limn_inf_sup u : cvgn u -> limn_inf u <= limn_sup u.
Proof.
Lemma cvg_limn_inf_sup u l : u @ \oo --> l -> (limn_inf u = l) * (limn_sup u = l).
Proof.
Lemma cvg_limn_infE u : cvgn u -> limn_inf u = limn u.
Proof.
Lemma cvg_limn_supE u : cvgn u -> limn_sup u = limn u.
Proof.
Lemma cvg_sups u l : u @ \oo --> l -> sups u @ \oo --> (l : R^o).
Proof.
Lemma cvg_infs u l : u @ \oo --> l -> infs u @ \oo --> (l : R^o).
Proof.
Lemma le_limn_supD u v : bounded_fun u -> bounded_fun v ->
limn_sup (u \+ v) <= limn_sup u + limn_sup v.
Proof.
Lemma le_limn_infD u v : bounded_fun u -> bounded_fun v ->
limn_inf u + limn_inf v <= limn_inf (u \+ v).
Proof.
Lemma limn_supD u v : cvgn u -> cvgn v ->
limn_sup (u \+ v) = limn_sup u + limn_sup v.
Proof.
Lemma limn_infD u v : cvgn u -> cvgn v ->
limn_inf (u \+ v) = limn_inf u + limn_inf v.
Proof.
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.
Proof.
Lemma einfsN u : einfs (-%E \o u) = -%E \o esups u.
Proof.
Lemma nonincreasing_esups u : nonincreasing_seq (esups u).
Proof.
Lemma nondecreasing_einfs u : nondecreasing_seq (einfs u).
Proof.
Lemma einfs_le_esups u n : einfs u n <= esups u n.
Proof.
Lemma cvg_esups_inf u : esups u @ \oo --> ereal_inf (range (esups u)).
Proof.
Lemma is_cvg_esups u : cvgn (esups u).
Proof.
Lemma cvg_einfs_sup u : einfs u @ \oo --> ereal_sup (range (einfs u)).
Proof.
Lemma is_cvg_einfs u : cvgn (einfs u).
Proof.
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[.
Proof.
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.
Proof.
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).
Proof.
Lemma limn_einf_lim u : limn_einf u = limn (einfs u).
Proof.
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.
Proof.
Lemma limn_esup_le_cvg u l : limn_esup u <= l -> (forall n, l <= u n) ->
u @ \oo --> l.
Proof.
Lemma limn_einfN u : limn_einf (-%E \o u) = - limn_esup u.
Proof.
Lemma limn_esupN u : limn_esup (-%E \o u) = - limn_einf u.
Proof.
Lemma limn_einf_sup u : limn_einf u <= limn_esup u.
Proof.
Lemma cvgNy_limn_einf_sup u : u @ \oo --> -oo ->
(limn_einf u = -oo) * (limn_esup u = -oo).
Proof.
Lemma cvgNy_einfs u : u @ \oo --> -oo -> einfs u @ \oo --> -oo.
Proof.
Lemma cvgNy_esups u : u @ \oo --> -oo -> esups u @ \oo --> -oo.
Proof.
Lemma cvgy_einfs u : u @ \oo --> +oo -> einfs u @ \oo --> +oo.
Proof.
Lemma cvgy_esups u : u @ \oo --> +oo -> esups u @ \oo --> +oo.
Proof.
Lemma cvg_esups u l : u @ \oo --> l -> esups u @ \oo --> l.
Proof.
Lemma cvg_einfs u l : u @ \oo --> l -> einfs u @ \oo --> l.
Proof.
Lemma cvg_limn_einf_sup u l : u @ \oo --> l ->
(limn_einf u = l) * (limn_esup u = l).
Proof.
Lemma is_cvg_limn_einfE u : cvgn u -> limn_einf u = limn u.
Proof.
Lemma is_cvg_limn_esupE u : cvgn u -> limn_esup u = limn u.
Proof.
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.
Proof.
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.
Proof.
Lemma contraction_dist n m : `|y n - y (n + m)| <= C * q%:num ^+ n.
Proof.
Lemma contraction_cvg : cvgn y.
Proof.
Lemma contraction_cvg_fixed : closed U -> limn y = f (limn y).
Proof.
End contractions.
Variable ctrf : is_contraction f.
Theorem banach_fixed_point : closed U -> U !=set0 -> exists2 p, U p & p = f p.
Proof.
End banach_contraction.