Challenge 9: Uniqueness of the limit
This week's challenge consists of proving in Lean 4 that if a sequence \(aₙ\) converges to both \(L\) and \(M\), then \(L = M\).
To do so, complete the following Lean 4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L M : ℝ} example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by sorry
1. Proof in natural language
We have to prove that if \(a_n\) is a sequence and \(L\) and \(M\) are limits of \(a_n\), then \(L = M\). We proceed by contradiction. To do so, assume that \[ L ≠ M \] Let \[ ε = |L - M| \tag{1} \] Then, \[ \frac{ε}{2} > 0 \tag{2} \] and, since \(a_n\) converges to \(L\) and to \(M\), there exist \(k₁\) and \(k₂\) such that \[ \begin{align} ∀ n ≥ k₁, |a_n - L| < \frac{ε}{2} \tag{3} \\ ∀ n ≥ k₂, |a_n - M| < \frac{ε}{2} \tag{4} \end{align} \] Let \[ k = \max(k₁, k₂) \tag{5} \] Then, \[ k ≥ k₁ \tag{6} \] \[ k ≥ k₂ \tag{7} \] From (3) and (6), we have \[ |aₖ - L| < \frac{ε}{2} \tag{8} \] From (4) and (7), we have \[ |aₖ - M| < \frac{ε}{2} \tag{9} \]
We have to derive a contradiction, for which it suffices to prove that \(ε < ε\). This is proved by the following chain \[ \begin{array}{llll} ε &= |L - M| &&\text{[by (1)]} \\ &= |(L - M) + (aₖ - aₖ)| \\ &= |(L - aₖ) + (aₖ - M)| \\ &≤ |L - aₖ| + |aₖ - M| \\ &= |aₖ - L| + |aₖ - M| \\ &< \frac{ε}{2} + \frac{ε}{2} &&\text{[by (8) and (9)]} \\ &= ε \end{array} \]
2. Proofs in Lean 4
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a : ℕ → ℝ} variable {L M : ℝ} -- Proof 1 -- ======= example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by by_contra h -- h : ¬L = M -- ⊢ False let ε := |L - M| apply lt_irrefl ε -- ⊢ ε < ε obtain ⟨k1, hk1⟩ := hL (ε/2) (by grind) -- k1 : ℕ -- hk1 : ∀ n ≥ k1, |a n - L| < ε / 2 obtain ⟨k2, hk2⟩ := hM (ε/2) (by grind) -- k2 : ℕ -- hk2 : ∀ n ≥ k2, |a n - M| < ε / 2 let k := max k1 k2 calc ε = |L - M| := rfl _ = |(L - M) + (a k - a k)| := by grind _ = |(L - a k) + (a k - M)| := by grind _ ≤ |L - a k| + |a k - M| := by grind _ = |a k - L| + |a k - M| := by grind _ < ε/2 + ε/2 := by grind _ = ε := by grind -- Proof 2 -- ======= example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by by_contra h -- h : ¬L = M -- ⊢ False let ε := |L - M| apply lt_irrefl ε -- ⊢ ε < ε obtain ⟨k1, hk1⟩ := hL (ε/2) (by grind) -- k1 : ℕ -- hk1 : ∀ n ≥ k1, |a n - L| < ε / 2 obtain ⟨k2, hk2⟩ := hM (ε/2) (by grind) -- k2 : ℕ -- hk2 : ∀ n ≥ k2, |a n - M| < ε / 2 let k := max k1 k2 calc ε = |(L - a k) + (a k - M)| := by grind _ < ε := by grind -- Proof 3 -- ======= example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by by_contra h -- h : ¬L = M -- ⊢ False let ε := |L - M| apply lt_irrefl ε -- ⊢ ε < ε have h1 : 0 < ε/2 := half_pos (abs_sub_pos.mpr h) obtain ⟨k1, hk1⟩ := hL (ε/2) h1 -- k1 : ℕ -- hk1 : ∀ n ≥ k1, |a n - L| < ε / 2 obtain ⟨k2, hk2⟩ := hM (ε/2) h1 -- k2 : ℕ -- hk2 : ∀ n ≥ k2, |a n - M| < ε / 2 let k := max k1 k2 have h2 : k ≥ k1 := le_max_left k1 k2 have h3 : k ≥ k2 := le_max_right k1 k2 have h4 : |a k - L| < ε/2 := hk1 k h2 have h5 : |a k - M| < ε/2 := hk2 k h3 calc ε = |L - M| := rfl _ = |(L - M) + (a k - a k)| := by ring_nf _ = |(L - a k) + (a k - M)| := by ring_nf _ ≤ |L - a k| + |a k - M| := abs_add_le (L - a k) (a k - M) _ = |a k - L| + |a k - M| := by congr 1 ; exact abs_sub_comm L (a k) _ < ε/2 + ε/2 := add_lt_add h4 h5 _ = ε := by ring -- Proof 4 -- ======= example (hL : SeqLim a L) (hM : SeqLim a M) : L = M := by by_contra h -- h : ¬L = M -- ⊢ False let ε := |L - M| apply lt_irrefl ε -- ⊢ ε < ε have h1 : 0 < ε/2 := half_pos (abs_sub_pos.mpr h) obtain ⟨k1, hk1⟩ := hL (ε/2) h1 -- k1 : ℕ -- hk1 : ∀ n ≥ k1, |a n - L| < ε / 2 obtain ⟨k2, hk2⟩ := hM (ε/2) h1 -- k2 : ℕ -- hk2 : ∀ n ≥ k2, |a n - M| < ε / 2 let k := max k1 k2 have h2 : k ≥ k1 := le_max_left k1 k2 have h3 : k ≥ k2 := le_max_right k1 k2 have h4 : |a k - L| < ε/2 := hk1 k h2 have h5 : |a k - M| < ε/2 := hk2 k h3 calc ε = |L - M| := rfl _ = |(L - M) + 0| := congrArg abs (add_zero (L - M)).symm _ = |(L - M) + (a k - a k)| := congrArg (|(L - M) + ·|) (sub_self (a k)).symm _ = |(L - a k) + (a k - M)| := congrArg abs (by ring) _ ≤ |L - a k| + |a k - M| := abs_add_le (L - a k) (a k - M) _ = |a k - L| + |a k - M| := congrArg (· + |a k - M|) (abs_sub_comm L (a k)) _ < ε/2 + ε/2 := add_lt_add h4 h5 _ = ε := add_halves ε -- Lemmas used -- =========== namespace Lemmas variable (a b c d : ℝ) variable (f : ℝ → ℝ) #check (abs_add_le a b : |a + b| ≤ |a| + |b|) #check (abs_sub_comm a b : |a - b| = |b - a|) #check (abs_sub_pos : 0 < |a - b| ↔ a ≠ b) #check (add_halves a : a / 2 + a / 2 = a) #check (add_lt_add : a < b → c < d → a + c < b + d) #check (add_zero a : a + 0 = a) #check (congrArg f : a = b → f a = f b) #check (half_pos : a > 0 → a / 2 > 0) #check (le_max_left a b : a ≤ max a b) #check (le_max_right a b : b ≤ max a b) #check (lt_irrefl a : ¬a < a) #check (sub_ne_zero_of_ne : a ≠ b → a - b ≠ 0) #check (sub_self a : a - a = 0) end Lemmas
The following video explains step by step how the solutions are built:
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.
3. Collaborative solutions
Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:
- Write your proof in live.lean-lang.org and check that it compiles without errors.
- Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean -- your proof ```
Comments