Challenge 18: Convergence of the product of convergent sequences
This week's challenge is to prove in Lean 4 that if the sequence \(aₙ\) converges to \(L\) and \(bₙ\) converges to \(M\), then \(aₙbₙ\) converges to \(LM\).
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 b c : ℕ → ℝ} variable {L M : ℝ} example (ha : SeqLim a L) (hb : SeqLim b M) (hc : ∀ n, c n = a n * b n) : SeqLim c (L * M) := by sorry
1. Proof in natural language
Let \(ε > 0\). Since \(a_n\) converges to \(L\), there exists \(N_1\) such that if \(n ≥ N_1\), then \[ |a_n − L| < 1 \] Therefore, for \(n ≥ N_1\) we have \[ \begin{array}{ll} |a_n| &= |a_n − L + L| \\ &≤ |a_n − L| + |L| \\ &< 1 + |L| \\ \end{array} \] Let us define \[ C = 1 + |L| \] Then \[ C > 0 \] and, for \(n ≥ N_1\) \[ |a_n| ≤ C \] Now, since \(a_n\) converges to \(L\), there exists \(N_2\) such that if \(n ≥ N_2\), then \[ |a_n − L| < \dfrac{ε}{2(|M| + 1)} \] On the other hand, since \(b_n\) converges to \(M\), there exists \(N_3\) such that if \(n ≥ N_3\), then \[ |b_n − M| < \dfrac{ε}{2C} \] Let \[ N = \max\{N_1,N_2,N_3\} \] If \(n ≥ N\), then the three previous inequalities hold. Now we estimate: \[ |a_nb_n − LM| \] Adding and subtracting \(a_nM\): \[ a_nb_n − LM = a_nb_n − a_nM + a_nM − LM \] Then \[ |a_nb_n − LM| = |a_n(b_n − M) + M(a_n − L)| \] By the triangle inequality, \[ |a_nb_n − LM| ≤ |a_n||b_n − M| +|M||a_n − L| \] Since \(n ≥ N_1\), we have \[ |a_n| ≤ C \] Hence, \[ |a_nb_n − LM| ≤ C|b_n − M| + |M||a_n − L| \] Using the chosen bounds, \[ \begin{array}{ll} C|b_n − M| &< C \dfrac{ε}{2C} \\ &= \dfrac{ε}{2} \end{array} \] and \[ |M||a_n − L| < |M| \dfrac{ε}{2(|M| + 1)} \] Since \[ \dfrac{|M|}{|M| + 1} < 1 \] it follows that \[ |M| \dfrac{ε}{2(|M| + 1)} < \dfrac{ε}{2} \] Therefore, \[ \begin{array}{ll} |a_nb_n − LM| &< \dfrac{ε}{2} + \dfrac{ε}{2} \\ &= ε \end{array} \] Thus, for every \(ε > 0\) there exists \(N\) such that if \(n ≥ N\), then \[ |a_nb_n − LM| < ε \] This proves that, for every \(ε > 0\), there exists \(N\) such that \(|a_nb_n − LM| < ε\) whenever \(n ≥ N\), that is, \(a_nb_n\) converges to \(LM\).
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 b c : ℕ → ℝ} variable {L M : ℝ} -- Proof 1 -- ======= example (ha : SeqLim a L) (hb : SeqLim b M) (hc : ∀ n, c n = a n * b n) : SeqLim c (L * M) := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |c n - L * M| < ε obtain ⟨N₁, hN₁⟩ := ha 1 (by positivity) -- N₁ : ℕ -- hN₁ : ∀ n ≥ N₁, |a n - L| < 1 have h1 : ∀ n ≥ N₁, |a n| < 1 + |L| := by grind set C := 1 + |L| -- h1 : ∀ n ≥ N₁, |a n| < C have h2 : C > 0 := by grind obtain ⟨N₂, hN₂⟩ := ha (ε / (2 * (|M| + 1))) (by positivity) -- N₂ : ℕ -- hN₂ : ∀ n ≥ N₂, |a n - L| < ε / (2 * (|M| + 1)) obtain ⟨N₃, hN₃⟩ := hb (ε / (2 * C)) (by positivity) -- N₃ : ℕ -- hN₃ : ∀ n ≥ N₃, |b n - M| < ε / (2 * C) set N := max N₁ (max N₂ N₃) use N -- ⊢ ∀ n ≥ N, |c n - L * M| < ε intro n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |c n - L * M| < ε have h3 : n ≥ N₁ := by grind have h4 : n ≥ N₂ := by grind have h5 : n ≥ N₃ := by grind have h6 : |a n| < C := by grind have h7 : |b n - M| < ε / (2 * C) := by grind have h8 : |a n - L| < ε / (2 * (|M| + 1)) := by grind have h9 : |M| * (ε / (2 * (|M| + 1))) < ε / 2 := by field_simp -- ⊢ |M| < |M| + 1 norm_num calc |c n - L * M| = |a n * b n - L * M| := by grind _ = |a n * (b n - M) + M * (a n - L)| := by grind _ ≤ |a n * (b n - M)| + |M * (a n - L)| := by grind _ = |a n| * |b n - M| + |M| * |a n - L| := by grind _ ≤ C * |b n - M| + |M| * |a n - L| := by gcongr _ < C * (ε / (2 * C)) + |M| * |a n - L| := by gcongr _ ≤ C * (ε / (2 * C)) + |M| * (ε / (2 * (|M| + 1))) := by gcongr _ = ε / 2 + |M| * (ε / (2 * (|M| + 1))) := by grind _ < ε / 2 + ε / 2 := by grind _ = ε := by grind -- Proof 2 -- ======= lemma L1 (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < 1 + |L| := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n| < |L| + 1 calc |a n| = |(a n - L) + L| := congrArg abs (sub_add_cancel (a n) L).symm _ ≤ |a n - L| + |L| := abs_add_le (a n - L) L _ < 1 + |L| := (add_lt_add_iff_right |L|).mpr (hk n hn) example (ha : SeqLim a L) (hb : SeqLim b M) (hc : ∀ n, c n = a n * b n) : SeqLim c (L * M) := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |c n - L * M| < ε obtain ⟨N₁, hN₁⟩ := L1 ha -- N₁ : ℕ -- hN₁ : ∀ n ≥ N₁, |a n| < 1 + |L| set C := 1 + |L| with hC -- hC : C = 1 + |L| have h2 : C > 0 := by positivity obtain ⟨N₂, hN₂⟩ := ha (ε / (2 * (|M| + 1))) (by positivity) -- N₂ : ℕ -- hN₂ : ∀ n ≥ N₂, |a n - L| < ε / (2 * (|M| + 1)) obtain ⟨N₃, hN₃⟩ := hb (ε / (2 * C)) (by positivity) -- N₃ : ℕ -- hN₃ : ∀ n ≥ N₃, |b n - M| < ε / (2 * C) set N := max N₁ (max N₂ N₃) use N -- ⊢ ∀ n ≥ N, |c n - L * M| < ε intro n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |c n - L * M| < ε have h3 : n ≥ N₁ := by omega have h4 : n ≥ N₂ := by omega have h5 : n ≥ N₃ := by omega have h6 : |a n| < C := by calc |a n| < 1 + |L| := hN₁ n h3 _ = C := rfl have h7 : |b n - M| < ε / (2 * C) := hN₃ n h5 have h8 : |a n - L| < ε / (2 * (|M| + 1)) := hN₂ n h4 have h9 : |M| * (ε / (2 * (|M| + 1))) < ε / 2 := by field_simp -- ⊢ |M| < |M| + 1 norm_num calc |c n - L * M| = |a n * b n - L * M| := congrArg (|· - L * M|) (hc n) _ = |a n * (b n - M) + M * (a n - L)| := by ring_nf _ ≤ |a n * (b n - M)| + |M * (a n - L)| := abs_add_le (a n * (b n - M)) (M * (a n - L)) _ = |a n| * |b n - M| + |M| * |a n - L| := by simp only [abs_mul] _ ≤ C * |b n - M| + |M| * |a n - L| := by gcongr _ < C * (ε / (2 * C)) + |M| * |a n - L| := by gcongr _ ≤ C * (ε / (2 * C)) + |M| * (ε / (2 * (|M| + 1))) := by gcongr _ = ε / 2 + |M| * (ε / (2 * (|M| + 1))) := by field_simp _ < ε / 2 + ε / 2 := by gcongr _ = ε := add_halves ε
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.