Skip to main content

Challenge 18: Convergence of the product of convergent sequences

Also available in:

Español

Prove 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 \] Hence, for \(n ≥ N_1\) we have \[ \begin{array}{ll} |a_n| &= |a_n − L + L| \\ &≤ |a_n − L| + |L| \\ &< 1 + |L| \\ \end{array} \] 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 : ℝ}

-- Solution 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

-- Solution 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.

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