theorem squeeze_converges {a b x : RealSequence} {l : ℝ} (hax : ∀ (n : ℕ), a n ≤ x n) (hxb : ∀ (n : ℕ), x n ≤ b n) (ha : ConvergesTo a l) (hb : ConvergesTo b l) : ConvergesTo x l

Lemma 2.2.1 (Squeeze lemma): If real sequences a, x, b satisfy a n ≤ x n ≤ b n for every n, and both a and b converge to the same limit l, then x also converges to l, so lim_{n → ∞} x_n = lim_{n → ∞} a_n = lim_{n → ∞} b_n.

theorem squeeze_convergentSequence {a b x : RealSequence} {l : ℝ} (hax : ∀ (n : ℕ), a n ≤ x n) (hxb : ∀ (n : ℕ), x n ≤ b n) (ha : ConvergesTo a l) (hb : ConvergesTo b l) : ConvergentSequence x

A sequence squeezed between two convergent sequences with common limit is itself convergent with that limit.

theorem inv_mul_sqrt_bounds (n : ℕ) : 0 ≤ 1 / ((↑n + 1) * √(↑n + 1)) ∧ 1 / ((↑n + 1) * √(↑n + 1)) ≤ 1 / (↑n + 1)

Example 2.2.2: By bounding 1 / (n √n) (starting at n = 1) between the constant 0 sequence and 1 / n, and using the squeeze lemma together with lim_{n → ∞} 1 / n = 0, we conclude lim_{n → ∞} 1 / (n √n) = 0.

theorem inv_mul_sqrt_converges_to_zero : ConvergesTo (fun (n : ℕ) => 1 / ((↑n + 1) * √(↑n + 1))) 0

theorem limit_le_of_pointwise_le {x y : RealSequence} {l m : ℝ} (hx : ConvergesTo x l) (hy : ConvergesTo y m) (hxy : ∀ (n : ℕ), x n ≤ y n) : l ≤ m

Lemma 2.2.3: If convergent real sequences x and y satisfy x n ≤ y n for every n, then their limits obey lim_{n → ∞} x_n ≤ lim_{n → ∞} y_n.

theorem limit_nonneg_of_pointwise_nonneg {x : RealSequence} {l : ℝ} (hx : ConvergesTo x l) (h_nonneg : ∀ (n : ℕ), 0 ≤ x n) : 0 ≤ l

A convergent sequence with pointwise nonnegative terms has a nonnegative limit.

theorem limit_lower_bound_of_pointwise {x : RealSequence} {a l : ℝ} (hx : ConvergesTo x l) (hax : ∀ (n : ℕ), a ≤ x n) : a ≤ l

A pointwise lower bound for a convergent sequence bounds its limit below.

theorem limit_upper_bound_of_pointwise {x : RealSequence} {b l : ℝ} (hx : ConvergesTo x l) (hxb : ∀ (n : ℕ), x n ≤ b) : l ≤ b

A pointwise upper bound for a convergent sequence bounds its limit above.

theorem limit_nonneg_and_between_bounds : (∀ {x : RealSequence} {l : ℝ}, ConvergesTo x l → (∀ (n : ℕ), 0 ≤ x n) → 0 ≤ l) ∧ ∀ {x : RealSequence} {a b l : ℝ}, ConvergesTo x l → (∀ (n : ℕ), a ≤ x n) → (∀ (n : ℕ), x n ≤ b) → a ≤ l ∧ l ≤ b

Corollary 2.2.4: (i) If a convergent real sequence has nonnegative terms, then its limit is nonnegative. (ii) If a convergent real sequence is bounded between real numbers a and b, then its limit also lies between a and b.

theorem limit_add_of_convergent {x y : RealSequence} {l m : ℝ} (hx : ConvergesTo x l) (hy : ConvergesTo y m) : ConvergesTo (fun (n : ℕ) => x n + y n) (l + m)

Proposition 2.2.5: For convergent real sequences x and y, the usual algebraic operations preserve convergence. (i) The sum sequence converges to the sum of the limits. (ii) The difference sequence converges to the difference of the limits. (iii) The termwise product converges to the product of the limits. (iv) If lim_{n → ∞} y_n ≠ 0 and every y n ≠ 0, then the quotient sequence converges to the quotient of the limits.

theorem limit_sub_of_convergent {x y : RealSequence} {l m : ℝ} (hx : ConvergesTo x l) (hy : ConvergesTo y m) : ConvergesTo (fun (n : ℕ) => x n - y n) (l - m)

The limit of the difference of two convergent real sequences is the difference of their limits.

theorem limit_mul_of_convergent {x y : RealSequence} {l m : ℝ} (hx : ConvergesTo x l) (hy : ConvergesTo y m) : ConvergesTo (fun (n : ℕ) => x n * y n) (l * m)

The limit of the termwise product of two convergent real sequences is the product of their limits.

theorem limit_div_of_convergent {x y : RealSequence} {l m : ℝ} (hx : ConvergesTo x l) (hy : ConvergesTo y m) (hm : m ≠ 0) (hy_ne_zero : ∀ (n : ℕ), y n ≠ 0) : ConvergesTo (fun (n : ℕ) => x n / y n) (l / m)

If a convergent real sequence y has nonzero limit and no zero terms, then the termwise quotient of convergent sequences x and y converges to the quotient of their limits.

theorem limit_sqrt_of_nonneg {x : RealSequence} {l : ℝ} (hx : ConvergesTo x l) (h_nonneg : ∀ (n : ℕ), 0 ≤ x n) : ConvergesTo (fun (n : ℕ) => √(x n)) √l

Proposition 2.2.6: If a convergent real sequence satisfies x n ≥ 0 for every n, then its termwise square roots converge to the square root of its limit, i.e. lim_{n → ∞} √(x_n) = √(lim_{n → ∞} x_n).

theorem limit_abs_of_convergent {x : RealSequence} {l : ℝ} (hx : ConvergesTo x l) : ConvergesTo (fun (n : ℕ) => |x n|) |l|

Proposition 2.2.7: If a real sequence x converges, then its termwise absolute values also converge, and the limit is the absolute value of the original limit, so lim_{n → ∞} |x_n| = |lim_{n → ∞} x_n|.

theorem abs_convergentSequence {x : RealSequence} (hx : ConvergentSequence x) : ConvergentSequence fun (n : ℕ) => |x n|

The absolute value of a convergent real sequence is also convergent.

noncomputable def sqrtTwoNewtonSequence : RealSequence

Example 2.2.8: Starting from x₁ = 2 and defining x_{n+1} = x_n - (x_n^2 - 2) / (2 x_n), the recursion is well-defined because each term stays positive. The sequence is monotone decreasing and bounded below, so it converges; taking limits in the recurrence gives x = √2, so the limit equals √2.

Equations

• sqrtTwoNewtonSequence n = Nat.recOn n 2 fun (x : ℕ) (x_n : ℝ) => x_n - (x_n ^ 2 - 2) / (2 * x_n)

theorem sqrtTwoNewtonSequence_pos (n : ℕ) : 0 < sqrtTwoNewtonSequence n

Every term of the Newton sequence for √2 is positive, so the recurrence is well-defined.

theorem sqrtTwoNewtonSequence_sq_sub_two_nonneg (n : ℕ) : 0 ≤ sqrtTwoNewtonSequence n ^ 2 - 2

For every n, (x_n)^2 - 2 is nonnegative along the Newton sequence.

theorem sqrtTwoNewtonSequence_monotone : MonotoneDecreasingSequence sqrtTwoNewtonSequence

The Newton sequence for √2 is monotone decreasing.

theorem sqrtTwoNewtonSequence_tendsto : ConvergesTo sqrtTwoNewtonSequence √2

The Newton sequence for √2 converges to √2.

theorem sqrtTwoNewtonSequence_converges : (∀ (n : ℕ), 0 < sqrtTwoNewtonSequence n) ∧ MonotoneDecreasingSequence sqrtTwoNewtonSequence ∧ ConvergesTo sqrtTwoNewtonSequence √2

The Newton sequence for √2 stays positive, decreases monotonically, and converges to √2.

def quadraticRecursiveSequence (x₁ : ℝ) : RealSequence

Example 2.2.9: For the recursion x_{n+1} = x_n^2 + x_n, starting at x₁ = 1 yields an unbounded sequence and hence no limit, while starting at x₁ = 0 gives the constant zero sequence whose limit is 0. The long-term behavior therefore depends on the initial value.

Equations

• quadraticRecursiveSequence x₁ n = Nat.recOn n x₁ fun (x : ℕ) (x_n : ℝ) => x_n ^ 2 + x_n

theorem quadraticRecursiveSequence_one_lower_bound (n : ℕ) : quadraticRecursiveSequence 1 n ≥ ↑n + 1

Lower bound for the quadratic recursion started at 1.

theorem quadraticRecursiveSequence_unbounded : ¬BoundedSequence (quadraticRecursiveSequence 1)

With initial value 1, the quadratic recursion grows without bound.

theorem quadraticRecursiveSequence_diverges : ¬ConvergentSequence (quadraticRecursiveSequence 1)

The quadratic recursion started at 1 does not converge.

theorem quadraticRecursiveSequence_zero_eq_zero (n : ℕ) : quadraticRecursiveSequence 0 n = 0

The quadratic recursion started at 0 is identically zero.

theorem quadraticRecursiveSequence_zero_converges : ConvergesTo (quadraticRecursiveSequence 0) 0

Starting the quadratic recursion at 0 yields a sequence converging to 0.

theorem converges_of_abs_sub_le_converging_to_zero {x a : RealSequence} {x₀ : ℝ} (ha : ConvergesTo a 0) (hbound : ∀ (n : ℕ), |x n - x₀| ≤ a n) : ConvergesTo x x₀

Proposition 2.2.10: If x is a real sequence and there exists x₀ : ℝ and a convergent sequence a with lim_{n → ∞} a_n = 0 such that |x_n - x₀| ≤ a_n for every n, then x converges to x₀.

theorem convergentSequence_of_abs_sub_le_converging_to_zero {x a : RealSequence} {x₀ : ℝ} (ha : ConvergesTo a 0) (hbound : ∀ (n : ℕ), |x n - x₀| ≤ a n) : ConvergentSequence x

A sequence controlled by a convergent error term with vanishing limit is convergent.

theorem pow_sequence_converges_or_unbounded {c : ℝ} (hc_pos : 0 < c) : (c < 1 → ConvergesTo (fun (n : ℕ) => c ^ n) 0) ∧ (1 < c → ¬BoundedSequence fun (n : ℕ) => c ^ n)

Proposition 2.2.11: Let c > 0. (i) If c < 1, then lim_{n → ∞} c^n = 0. (ii) If c > 1, then the sequence (c^n) is unbounded.

theorem ratio_test_for_sequences {x : RealSequence} {L : ℝ} (hx_ne : ∀ (n : ℕ), x n ≠ 0) (hL : ConvergesTo (fun (n : ℕ) => |x (n + 1)| / |x n|) L) : (L < 1 → ConvergesTo x 0) ∧ (1 < L → ¬BoundedSequence x)

Lemma 2.2.12 (Ratio test for sequences): For a real sequence x with no zero terms, suppose the limit L = lim_{n → ∞} |x_{n+1}| / |x_n| exists. (i) If L < 1, then x converges to 0. (ii) If L > 1, then x is unbounded and therefore diverges.

theorem pow_two_over_factorial_nonzero (n : ℕ) : 2 ^ n / ↑n.factorial ≠ 0

Example 2.2.13: Applying the ratio test with |x_{n+1}| / |x_n| = 2 / (n + 1), we obtain lim_{n → ∞} (2^n / n!) = 0.

theorem pow_two_over_factorial_ratio_limit : ConvergesTo (fun (n : ℕ) => |2 ^ (n + 1) / ↑(n + 1).factorial| / |2 ^ n / ↑n.factorial|) 0

theorem pow_two_over_factorial_converges_to_zero : ConvergesTo (fun (n : ℕ) => 2 ^ n / ↑n.factorial) 0

theorem nth_root_sequence_converges_to_one : ConvergesTo (fun (n : ℕ) => (↑n + 1).rpow (1 / (↑n + 1))) 1

Example 2.2.14: Using the ratio test on the sequence (n / (1 + ε)^n), for any ε > 0 we get n / (1 + ε)^n → 0, which forces 1 ≤ n^(1/n) < 1 + ε for large n. Hence lim_{n → ∞} n^(1/n) = 1.