The upper tail supremum sequence a_n = sup { x_k | k ≥ n } attached to a
real sequence x.
Instances For
The lower tail infimum sequence b_n = inf { x_k | k ≥ n } attached to a
real sequence x.
Instances For
The limit superior of a real sequence, realized as the infimum of the tail suprema.
Equations
- limsupSequence x = sInf (Set.range (tailSupSequence x))
Instances For
The limit inferior of a real sequence, realized as the supremum of the tail infima.
Equations
- liminfSequence x = sSup (Set.range (tailInfSequence x))
Instances For
Proposition 2.3.2: For a bounded sequence {x_n}, with a_n the tail
suprema and b_n the tail infima as above: (i) {a_n} is bounded and
monotone decreasing while {b_n} is bounded and monotone increasing, so
liminf_{n → ∞} x_n and limsup_{n → ∞} x_n exist; (ii)
limsup_{n → ∞} x_n = inf { a_n : n ∈ ℕ } and
liminf_{n → ∞} x_n = sup { b_n : n ∈ ℕ }; (iii)
liminf_{n → ∞} x_n ≤ limsup_{n → ∞} x_n.
Definition 2.3.1: For a bounded real sequence {x_n}, define the tail
suprema a_n = sup { x_k | k ≥ n } and tail infima b_n = inf { x_k | k ≥ n }.
When the limits of these tails exist, set
limsup_{n → ∞} x_n = lim_{n → ∞} a_n and
liminf_{n → ∞} x_n = lim_{n → ∞} b_n.
Example 2.3.3: For the sequence defined by
xₙ = (n + 1) / n when n is odd and xₙ = 0 when n is even, the limit
inferior is 0, the limit superior is 1, and the sequence does not
converge.
Instances For
The terms of the sequence in Example 2.3.3 are nonnegative and bounded by
2.
Every tail infimum of the sequence in Example 2.3.3 equals 0.
The tail supremum sequence in Example 2.3.3 converges to 1.
Example 2.3.3, continued: the sequence above has liminf = 0, limsup = 1
and is divergent.
Theorem 2.3.4: For a bounded sequence {x_n}, there is a subsequence whose
limit equals limsup_{n → ∞} x_n, and (possibly another) subsequence whose
limit equals liminf_{n → ∞} x_n.
Proposition 2.3.5: A bounded sequence {x_n} converges if and only if its
limit inferior and limit superior coincide. Moreover, when {x_n} converges
to L, this common value equals L.
See Proposition 2.3.5: for a bounded sequence that converges to L, the
limit equals both the limit inferior and the limit superior.
Proposition 2.3.6: For a bounded sequence {x_n} and any subsequence
{x_{n_k}}, the limit inferior of the original sequence bounds below the
subsequence's limit inferior, which in turn does not exceed its limit
superior, and this limit superior is bounded above by the limit superior of
the original sequence.
Theorem 2.3.8 (Bolzano--Weierstrass): Every bounded real sequence
{x_n} admits a convergent subsequence {x_{n_i}}.
Proposition 2.3.7: A bounded sequence {x_n} converges to x if and only if
every convergent subsequence {x_{n_k}} converges to the same limit x.
Definition 2.3.9: A real sequence {x_n} diverges to +∞ if for every
K : ℝ there exists M : ℕ such that x n > K for all n ≥ M; we then
write lim_{n → ∞} x_n = ∞. It diverges to -∞ if for every K : ℝ there
is M : ℕ with x n < K for all n ≥ M, written lim_{n → ∞} x_n = -∞.
Equations
- DivergesToInfinitySequence x = ∀ (K : ℝ), ∃ (M : ℕ), ∀ n ≥ M, K < x n
Instances For
A real sequence diverges to negative infinity when its terms eventually stay below every real threshold.
Equations
- DivergesToMinusInfinitySequence x = ∀ (K : ℝ), ∃ (M : ℕ), ∀ n ≥ M, x n < K
Instances For
Proposition 2.3.10: A monotone unbounded sequence diverges to an infinite
limit. If {x_n} is monotone increasing and unbounded above, then
lim_{n → ∞} x_n = ∞; if it is monotone decreasing and unbounded below, then
lim_{n → ∞} x_n = -∞.
See Proposition 2.3.10: a monotone decreasing sequence without a lower
bound diverges to -∞.
The book's notion of divergence to +∞ agrees with Filter.Tendsto to
Filter.atTop.
The book's notion of divergence to -∞ agrees with Filter.Tendsto to
Filter.atBot.
Example 2.3.11: the sequences n and n^2 diverge to +∞, while the
sequence -n diverges to -∞.
Definition 2.3.12: For an unbounded real sequence {xₙ}, set
aₙ = sup { x_k | k ≥ n } and bₙ = inf { x_k | k ≥ n }, where the suprema and
infima are taken in the extended real numbers. The limit superior is
inf { aₙ : n ∈ ℕ } and the limit inferior is sup { bₙ : n ∈ ℕ }.
Instances For
See the preceding comment: the lower tail infimum in the extended reals.
Instances For
The limit superior of a (possibly unbounded) real sequence, valued in ℝ∞.
Equations
Instances For
The limit inferior of a (possibly unbounded) real sequence, valued in ℝ∞.
Equations
Instances For
The extended-real limsup defined via tail suprema coincides with the
Filter.limsup of the sequence viewed in ℝ∞.
The extended-real liminf defined via tail infima coincides with the
Filter.liminf of the sequence viewed in ℝ∞.
Proposition 2.3.13: For an unbounded sequence {x_n} with tail suprema
a_n = sup { x_k | k ≥ n } and tail infima b_n = inf { x_k | k ≥ n }
formed in the extended reals, the sequence {a_n} is decreasing and {b_n}
is increasing. If every a_n is a (finite) real number, then
limsup_{n → ∞} x_n = lim_{n → ∞} a_n; if every b_n is real, then
liminf_{n → ∞} x_n = lim_{n → ∞} b_n.
Example 2.3.14: For xₙ = 0 when n is odd and xₙ = n when n is
even, each tail supremum aₙ equals ∞ because even indices keep growing,
while each tail infimum bₙ is 0 thanks to the odd indices. Consequently,
limsup_{n → ∞} xₙ = ∞, liminf_{n → ∞} xₙ = 0, and the sequence is
divergent.