def CauchySequence (x : RealSequence) : Prop

Definition 2.4.1: A real sequence {xₙ} is called a Cauchy sequence if for every ε > 0 there exists M ∈ ℕ such that for all n, k ≥ M we have |x n - x k| < ε.

Equations

• CauchySequence x = ∀ ε > 0, ∃ (M : ℕ), ∀ ⦃n k : ℕ⦄, M ≤ n → M ≤ k → |x n - x k| < ε

theorem cauchySequence_iff_cauchySeq (x : RealSequence) : CauchySequence x ↔ CauchySeq x

The book's notion of a Cauchy sequence of real numbers coincides with the standard CauchySeq predicate from mathlib.

theorem example_242_one_div_nat_cauchy : CauchySequence fun (n : ℕ) => 1 / ↑n.succ

Example 2.4.2: The sequence 1 / n (with indexing starting at n = 1) is Cauchy.

theorem neg_one_pow_even_odd (m : ℕ) : (-1) ^ (2 * m) = 1 ∧ (-1) ^ (2 * m + 1) = -1

Explicit values of consecutive even and odd powers of -1.

theorem neg_one_pow_consecutive_abs (m : ℕ) : |(-1) ^ (2 * m) - (-1) ^ (2 * m + 1)| = 2

The absolute difference of consecutive powers of -1 is 2.

theorem example_243_neg_one_pow_not_cauchy : ¬CauchySequence fun (n : ℕ) => (-1) ^ n.succ

Example 2.4.3: The sequence { (-1)^n }_{n = 1}^∞ is not Cauchy.

theorem cauchySequence_bounded {x : RealSequence} (hx : CauchySequence x) : BoundedSequence x

Proposition 2.4.4: Every Cauchy real sequence is bounded.

theorem convergentSequence_cauchySequence {x : RealSequence} : ConvergentSequence x → CauchySequence x

A convergent real sequence is Cauchy (ε/2 argument).

theorem cauchySequence_convergentSequence {x : RealSequence} : CauchySequence x → ConvergentSequence x

A Cauchy real sequence converges by completeness of ℝ.

theorem cauchySequence_iff_convergentSequence (x : RealSequence) : CauchySequence x ↔ ConvergentSequence x

Theorem 2.4.5: A sequence of real numbers is Cauchy if and only if it converges (using completeness of ℝ).