Challenge 21: Subsequences have the same limit as the sequence
A subsequence is obtained by applying an extraction function to the original sequence; that is, a strictly increasing function \(φ : ℕ \to ℕ\). For example, the subsequence \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] is obtained with the extraction function \(\varphi\) defined by \(\varphi(n) = 2n\).
The above definitions are formalized in Lean 4 as:
-- φ is an extraction function. def IsExtraction (φ : ℕ → ℕ) := StrictMono φ -- v is a subsequence of u. def Subseq (v u : ℕ → ℝ) := ∃ φ, IsExtraction φ ∧ v = u ∘ φ -- a is the limit of u. def SeqLim (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε
Prove that every subsequence of a convergent sequence converges to the same limit as the sequence.
To do this, complete the following Lean 4 theory:
import Mathlib.Data.Real.Basic variable {u v : ℕ → ℝ} variable {a : ℝ} -- φ is an extraction function. def extraction (φ : ℕ → ℕ) := StrictMono φ -- v is a subsequence of u. def subsequence (v u : ℕ → ℝ) := ∃ φ, extraction φ ∧ v = u ∘ φ -- a is the limit of u. def SeqLimit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε example (hv : subsequence v u) (ha : SeqLimit u a) : SeqLimit v a := by sorry
1. Proof in natural language
We will use the following lemma: if \(φ\) is an extraction function, then \[ ∀ n, n ≤ φ(n) \]
Since \(v\) is a subsequence of \(u\), there is an extraction function \(φ\) such that \[ v = u ∘ φ \tag{1} \]
We have to prove that for every \(ε > 0\) there is a \(k ∈ ℕ\) such that \[ ∀ n ≥ k, |v(n) - a| < ε \tag{2} \]
Since \(a\) is the limit of \(u\), there is a \(k ∈ ℕ\) such that \[ ∀ n ≥ k, |u(n) - a| < ε \tag{3} \]
We show that this \(k\) satisfies (2). Let \(n ≥ k\). Then \[ φ(n) ≥ k \tag{4} \] since \[ φ(n) ≥ n ≥ k \quad\text{[by the lemma]} \] Hence, \[ \begin{array}{ll} |v(n) - a| &= |(u ∘ φ)(n) - a| &&\text{[by (1)]} \\ &= |u(φ(n)) - a| \\ &< ε &&\text{[by (3) and (4)]} \end{array} \]
2. Proofs in Lean 4
import Mathlib.Data.Real.Basic variable {u v : ℕ → ℝ} variable {a : ℝ} -- φ is an extraction function. def extraction (φ : ℕ → ℕ) := StrictMono φ -- v is a subsequence of u. def subsequence (v u : ℕ → ℝ) := ∃ φ, extraction φ ∧ v = u ∘ φ -- a is the limit of u. def SeqLimit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε -- Proof 1 -- ======= example (hv : subsequence v u) (ha : SeqLimit u a) : SeqLimit v a := by obtain ⟨φ, hφ, hφ'⟩ := hv -- φ : ℕ → ℕ -- hφ : extraction φ -- hφ' : v = u ∘ φ intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |v n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε use k -- ⊢ ∀ n ≥ k, |v n - a| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |v n - a| < ε have h1 : φ n ≥ k := calc φ n ≥ n := StrictMono.le_apply hφ _ ≥ k := hn calc |v n - a| = |(u ∘ φ ) n - a| := by rw [hφ'] _ = |u (φ n) - a| := rfl _ < ε := hk (φ n) h1 -- Proof 2 -- ======= example (hv : subsequence v u) (ha : SeqLimit u a) : SeqLimit v a := by obtain ⟨φ, hφ, rfl⟩ := hv -- φ : ℕ → ℕ -- hφ : extraction φ -- ⊢ SeqLimit (u ∘ φ) a intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε use k -- ⊢ ∀ n ≥ k, |(u ∘ φ) n - a| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |(u ∘ φ) n - a| < ε have h1 : φ n ≥ k := calc φ n ≥ n := hφ.le_apply _ ≥ k := hn calc |(u ∘ φ) n - a| _ = |u (φ n) - a| := rfl _ < ε := hk (φ n) h1 -- Proof 3 -- ======= example (hv : subsequence v u) (ha : SeqLimit u a) : SeqLimit v a := by obtain ⟨φ, hφ, rfl⟩ := hv -- φ : ℕ → ℕ -- hφ : extraction φ -- ⊢ SeqLimit (u ∘ φ) a intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε use k -- ⊢ ∀ n ≥ k, |(u ∘ φ) n - a| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |(u ∘ φ) n - a| < ε apply hk -- ⊢ φ n ≥ k apply le_trans hn -- ⊢ n ≤ φ n exact hφ.le_apply -- Proof 4 -- ======= example (hv : subsequence v u) (ha : SeqLimit u a) : SeqLimit v a := by obtain ⟨φ, hφ, rfl⟩ := hv -- φ : ℕ → ℕ -- hφ : extraction φ -- ⊢ SeqLimit (u ∘ φ) a intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε exact ⟨k, fun n hn ↦ hk (φ n) (le_trans hn hφ.le_apply)⟩
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.