@[reducible, inline]

abbrev RealSequence : Type

Definition 2.1.1: A sequence of real numbers is a function x : ℕ → ℝ, whose n-th term is denoted x n (often written xₙ), and also denoted {x_n}_{n=1}^{\infty}. The sequence is bounded if there exists B : ℝ with |x n| ≤ B for all n. It is bounded below if there is B with B ≤ x n for all n, and bounded above if there is B with x n ≤ B for all n.

Equations

• RealSequence = (ℕ → ℝ)

def BoundedSequence (x : RealSequence) : Prop

A real sequence admitting a uniform bound on absolute values.

Equations

• BoundedSequence x = ∃ (B : ℝ), ∀ (n : ℕ), |x n| ≤ B

def BoundedBelowSequence (x : RealSequence) : Prop

A real sequence with a uniform lower bound.

Equations

• BoundedBelowSequence x = ∃ (B : ℝ), ∀ (n : ℕ), B ≤ x n

def BoundedAboveSequence (x : RealSequence) : Prop

A real sequence with a uniform upper bound.

Equations

• BoundedAboveSequence x = ∃ (B : ℝ), ∀ (n : ℕ), x n ≤ B

theorem real_mem_closedBall_0_iff_abs_le (x B : ℝ) : x ∈ Metric.closedBall 0 B ↔ |x| ≤ B

Closed balls at the origin are described by absolute values.

theorem range_subset_closedBall_iff_abs_bound (x : ℕ → ℝ) (B : ℝ) : Set.range x ⊆ Metric.closedBall 0 B ↔ ∀ (n : ℕ), |x n| ≤ B

Range inclusion in a closed ball is equivalent to a uniform absolute bound.

theorem boundedSequence_iff_isBounded_range (x : RealSequence) : BoundedSequence x ↔ Bornology.IsBounded (Set.range x)

A bounded real sequence in the book's sense is equivalent to the image of the sequence being bounded as a subset of ℝ.

theorem boundedAboveSequence_iff_bddAbove_range (x : RealSequence) : BoundedAboveSequence x ↔ BddAbove (Set.range x)

A sequence is bounded above exactly when its range is bounded above as a subset of ℝ.

theorem boundedBelowSequence_iff_bddBelow_range (x : RealSequence) : BoundedBelowSequence x ↔ BddBelow (Set.range x)

A sequence is bounded below exactly when its range is bounded below as a subset of ℝ.

def ConvergesTo (x : RealSequence) (l : ℝ) : Prop

Definition 2.1.2: A real sequence x converges to l if for every ε > 0 there is an M : ℕ such that |x n - l| < ε whenever n ≥ M. Such an l is called a limit of the sequence, and a sequence with some limit is called convergent (otherwise divergent).

Equations

• ConvergesTo x l = ∀ ε > 0, ∃ (M : ℕ), ∀ n ≥ M, |x n - l| < ε

def ConvergentSequence (x : RealSequence) : Prop

A real sequence is convergent if it admits a (necessarily unique) limit.

Equations

• ConvergentSequence x = ∃ (l : ℝ), ConvergesTo x l

theorem convergesTo_iff_tendsto (x : RealSequence) (l : ℝ) : ConvergesTo x l ↔ Filter.Tendsto x Filter.atTop (nhds l)

The book's ε–M definition of convergence agrees with the standard Filter.Tendsto formulation in mathlib.

theorem constant_seq_converges (a : ℝ) : ConvergesTo (fun (x : ℕ) => a) a

A constant real sequence converges to its constant value.

theorem constant_one_converges : ConvergesTo (fun (x : ℕ) => 1) 1

Example 2.1.3: The constant sequence 1, 1, 1, … converges to 1; for any ε > 0 one may take M = 1, giving |x n - x| = |1 - 1| < ε for every n.

theorem tendsto_inv_nat_succ : Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhds 0)

Example 2.1.4: The sequence x n = 1 / n (starting at n = 1) is convergent with limit 0; the proof picks M with 1 / M < ε by the Archimedean property and then estimates |x n - 0| ≤ 1 / M for all n ≥ M.

theorem inv_nat_converges_to_zero : ConvergesTo (fun (n : ℕ) => 1 / (↑n + 1)) 0

theorem alternating_signs_diverges : ¬ConvergentSequence fun (n : ℕ) => (-1) ^ n

Example 2.1.5: The alternating sign sequence {(-1)^n} is divergent. If it had a limit x, then taking ε = 1/2 and comparing an even term and the next odd term would force both |1 - x| < 1/2 and |-1 - x| < 1/2, which is impossible.

theorem convergesTo_unique {x : RealSequence} {l l' : ℝ} (h₁ : ConvergesTo x l) (h₂ : ConvergesTo x l') : l = l'

Proposition 2.1.6: A convergent sequence has a unique limit. If a real sequence converges to both l and l', then l = l'.

theorem convergentSequence_bounded {x : RealSequence} (hx : ConvergentSequence x) : BoundedSequence x

Proposition 2.1.7: Every convergent real sequence is bounded.

theorem quadratic_fraction_abs_sub_eq (n : ℕ) : |((↑n + 1) ^ 2 + 1) / ((↑n + 1) ^ 2 + (↑n + 1)) - 1| = ↑n / ((↑n + 1) ^ 2 + (↑n + 1))

theorem quadratic_fraction_abs_le_inv (n : ℕ) : |((↑n + 1) ^ 2 + 1) / ((↑n + 1) ^ 2 + (↑n + 1)) - 1| ≤ 1 / (↑n + 1)

theorem quadratic_fraction_converges_to_one : ConvergesTo (fun (n : ℕ) => ((↑n + 1) ^ 2 + 1) / ((↑n + 1) ^ 2 + (↑n + 1))) 1

Example 2.1.8: The sequence ((n^2 + 1) / (n^2 + n)) (starting at n = 1) converges to 1; choosing M with 1 / M < ε yields | (n^2 + 1) / (n^2 + n) - 1 | < ε for all n ≥ M.

def MonotoneIncreasingSequence (x : RealSequence) : Prop

Definition 2.1.9: A sequence {x_n} is monotone increasing if x n ≤ x (n + 1) for every n, monotone decreasing if x n ≥ x (n + 1) for every n, and monotone if it is either monotone increasing or monotone decreasing.

Equations

• MonotoneIncreasingSequence x = ∀ (n : ℕ), x n ≤ x (n + 1)

def MonotoneDecreasingSequence (x : RealSequence) : Prop

A real sequence with nonincreasing successive terms.

Equations

• MonotoneDecreasingSequence x = ∀ (n : ℕ), x n ≥ x (n + 1)

def MonotoneSequence (x : RealSequence) : Prop

A real sequence that is either increasing or decreasing.

Equations

• MonotoneSequence x = (MonotoneIncreasingSequence x ∨ MonotoneDecreasingSequence x)

theorem monotoneIncreasingSequence_tendsto_sup {x : RealSequence} (hx : MonotoneIncreasingSequence x) (hB : BoundedSequence x) : ConvergesTo x (sSup (Set.range x))

A bounded monotone increasing real sequence converges to the supremum of its range.

theorem monotoneDecreasingSequence_tendsto_inf {x : RealSequence} (hx : MonotoneDecreasingSequence x) (hB : BoundedSequence x) : ConvergesTo x (sInf (Set.range x))

A bounded monotone decreasing real sequence converges to the infimum of its range.

theorem monotone_sequence_bounded_iff_convergent {x : RealSequence} (hx : MonotoneSequence x) : BoundedSequence x ↔ ConvergentSequence x

Theorem 2.1.10 (monotone convergence theorem): A monotone sequence {x_n} is bounded if and only if it is convergent. If {x_n} is monotone increasing and bounded, then its limit equals sup {x_n : n ∈ ℕ}; if monotone decreasing and bounded, then its limit equals inf {x_n : n ∈ ℕ}.

theorem monotoneIncreasingSequence_iff_monotone (x : RealSequence) : MonotoneIncreasingSequence x ↔ Monotone x

The book's notion of a monotone increasing sequence agrees with Monotone on ℕ.

theorem monotoneDecreasingSequence_iff_antitone (x : RealSequence) : MonotoneDecreasingSequence x ↔ Antitone x

The book's notion of a monotone decreasing sequence agrees with Antitone on ℕ.

theorem inv_sqrt_sequence_converges : (MonotoneDecreasingSequence fun (n : ℕ) => 1 / √(↑n + 1)) ∧ (BoundedBelowSequence fun (n : ℕ) => 1 / √(↑n + 1)) ∧ ConvergesTo (fun (n : ℕ) => 1 / √(↑n + 1)) 0

Example 2.1.11: The sequence x n = 1 / √(n + 1) is bounded below by 0, monotone decreasing since √(n + 2) ≥ √(n + 1), and hence bounded. By the monotone convergence theorem its limit equals its infimum, which is 0, so lim_{n → ∞} 1 / √(n + 1) = 0.

theorem harmonic_partial_sums_unbounded : (MonotoneIncreasingSequence fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), 1 / (↑k + 1)) ∧ ¬BoundedAboveSequence fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), 1 / (↑k + 1)

Example 2.1.12: The harmonic partial sums 1 + 1/2 + … + 1/n form a monotone increasing sequence. Although the growth is slow, the sequence is not bounded above and therefore does not converge; this unboundedness will be proved later using series.

theorem exists_monotone_sequences_tendsto_sup_inf {S : Set ℝ} (hS : S.Nonempty) (hbounded : Bornology.IsBounded S) : ∃ (x : RealSequence) (y : RealSequence), (∀ (n : ℕ), x n ∈ S) ∧ (∀ (n : ℕ), y n ∈ S) ∧ MonotoneIncreasingSequence x ∧ MonotoneDecreasingSequence y ∧ ConvergesTo x (sSup S) ∧ ConvergesTo y (sInf S)

Proposition 2.1.13: For a nonempty bounded subset S ⊆ ℝ there are monotone sequences {x_n} and {y_n} with terms in S such that lim_{n → ∞} x_n = sup S and lim_{n → ∞} y_n = inf S.

def sequenceTail (x : RealSequence) (K : ℕ) : RealSequence

Definition 2.1.14: For a real sequence x and K ∈ ℕ, the K-tail (tail) is the sequence starting at the (K+1)-st term, written {x_{n+K}}_{n=1}^{∞} or {x_n}_{n=K+1}^{∞}.

Equations

• sequenceTail x K n = x (n + (K + 1))

theorem convergesTo_tail_of_converges {x : RealSequence} {l : ℝ} (K : ℕ) (hx : ConvergesTo x l) : ConvergesTo (sequenceTail x K) l

A convergent sequence remains convergent after removing finitely many initial terms; the limit is unchanged.

theorem convergesTo_of_tail_converges {x : RealSequence} {l : ℝ} (K : ℕ) (hK : ConvergesTo (sequenceTail x K) l) : ConvergesTo x l

If a tail of a sequence converges, then so does the whole sequence, with the same limit.

theorem convergentSequence_iff_all_tails_converge (x : RealSequence) : ConvergentSequence x ↔ ∀ (K : ℕ), ConvergentSequence (sequenceTail x K)

Proposition 2.1.15: For a real sequence {x_n}, the following are equivalent: (i) the sequence converges; (ii) every K-tail {x_{n+K}}_{n=1}^{∞} converges for all K ∈ ℕ; (iii) some K-tail converges. Moreover, whenever these limits exist, they agree for all K, so lim_{n → ∞} x_n = lim_{n → ∞} x_{n+K}.

theorem convergentSequence_iff_exists_tail_converges (x : RealSequence) : ConvergentSequence x ↔ ∃ (K : ℕ), ConvergentSequence (sequenceTail x K)

If some tail of a real sequence converges, then the entire sequence converges, and conversely a convergent sequence has a convergent tail.

theorem convergesTo_tail_limit_eq {x : RealSequence} {l l' : ℝ} (K : ℕ) (hx : ConvergesTo x l) (hK : ConvergesTo (sequenceTail x K) l') : l = l'

Any limit of a sequence agrees with the limit of each of its tails.

structure RealSubsequence (x : RealSequence) : Type

Definition 2.1.16: Given a real sequence {x_n} and a strictly increasing sequence of indices n₁ < n₂ < n₃ < …, the extracted sequence i ↦ x (n i) is called a subsequence of {x_n}.

• indices : ℕ → ℕ

  the strictly increasing indexing function n_i selecting terms of the original sequence

• strictlyIncreasing : StrictMono self.indices

theorem subsequence_indices_ge_self {x : RealSequence} (s : RealSubsequence x) (i : ℕ) : i ≤ s.indices i

The indices of a subsequence eventually dominate their position: i ≤ n_i for all i.

def RealSubsequence.asSequence {x : RealSequence} (s : RealSubsequence x) : RealSequence

The subsequence of x determined by the index data s.

Equations

• s.asSequence i = x (s.indices i)

def IsRealSubsequence (x y : RealSequence) : Prop

A real sequence y is a subsequence of x if it arises by composing x with a strictly increasing index map.

Equations

• IsRealSubsequence x y = ∃ (s : RealSubsequence x), y = s.asSequence

theorem convergesTo_subsequence {x : RealSequence} {l : ℝ} (hx : ConvergesTo x l) (s : RealSubsequence x) : ConvergesTo s.asSequence l

Proposition 2.1.17: If a real sequence {x_n} converges, then every strictly increasing subsequence {x_{n_i}} also converges, with the same limit as the original sequence: lim_{n → ∞} x_n = lim_{i → ∞} x_{n_i}.

def alternatingZeroOneSequence : RealSequence

Example 2.1.18: A sequence can have convergent subsequences without being convergent itself. The alternating sequence 0, 1, 0, 1, … is defined by x n = 0 for odd n and x n = 1 for even n; its even-indexed subsequence converges to 1, its odd-indexed subsequence converges to 0, but the full sequence is divergent. Compare Proposition 2.1.15.

Equations

• alternatingZeroOneSequence n = if n % 2 = 0 then 1 else 0

theorem alternatingZeroOne_subsequences_converge : ¬ConvergentSequence alternatingZeroOneSequence ∧ ConvergesTo (fun (i : ℕ) => alternatingZeroOneSequence (2 * i)) 1 ∧ ConvergesTo (fun (i : ℕ) => alternatingZeroOneSequence (2 * i + 1)) 0

The alternating zero–one sequence diverges, even though its even subsequence converges to 1 and its odd subsequence converges to 0.