Skip to main content

If aₙ converges to L and bₙ to M, then aₙ+bₙ converges to L+M.

Also available in:

Español

Prove that if \(aₙ\) converges to \(L\) and \(bₙ\) to \(M\), then \(aₙ+bₙ\) converges to \(L+M\).

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {a b c : ℕ → ℝ}
variable {L M : ℝ}

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  sorry

1. Proof in natural language

We have to prove that for every \(ε ∈ ℝ\), if \[ ε > 0 \tag{1} \] then \[ (∃N ∈ ℕ)(∀n ∈ ℕ)[n ≥ N → |(a + b)(n) - (L + M)| < ε] \tag{2} \]

By (1), we have \[ \frac{ε}{2} > 0 \tag{3} \] By (3) and since the limit of \(a\) is \(L\), we have \[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |a(n) - L| < \frac{ε}{2}\right] \] Let \(N₁ ∈ ℕ\) be such that \[ (∀n ∈ ℕ)[n ≥ N₁ → |a(n) - L| < \frac{ε}{2}] \tag{4} \] By (3) and since the limit of \(b\) is \(M\), we have \[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |b(n) - M| < \frac{ε}{2}\right] \] Let \(N₂ ∈ ℕ\) be such that \[ (∀n ∈ ℕ)\left[n ≥ N₂ → |b(n) - M| < \frac{ε}{2}\right] \tag{5} \] Let \(N = max(N₁, N₂)\). We show that it satisfies condition (2). To do so, let \(n ∈ ℕ\) be such that \(n ≥ N\). Then, \(n ≥ N₁\) and \(n ≥ N₂\). Therefore, by properties (4) and (5) we have \begin{align} &|a(n) - L| < \frac{ε}{2} \tag{6} \newline &|b(n) - M| < \frac{ε}{2} \tag{7} \end{align} Finally, \begin{align} |(a + b)(n) - (L + M)| &= |(a(n) + b(n)) - (L + M)| \newline &= |(a(n) - L) + (b(n) - M)| \newline &≤ |a(n) - L| + |b(n) - M| \newline &< \frac{ε}{2} + \frac{ε}{2} &\text{[by (6) and (7)]} \newline &= ε \end{align}

2. Proofs in Lean 4

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {a b c : ℕ → ℝ}
variable {L M : ℝ}

def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

-- Proof 1
-- =======

namespace Solution1

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε / 2) (by linarith)
  -- Na : ℕ
  -- hNa : ∀ (n : ℕ), n ≥ Na → |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε / 2) (by linarith)
  -- Nb : ℕ
  -- hNb : ∀ (n : ℕ), n ≥ Nb → |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ (n : ℕ), n ≥ max Na Nb → |(s + t) n - (L + M)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |(a + b) n - (L + M)| < ε
  calc |(a + b) n - (L + M)|
     = |(a n + b n) - (L + M)|  := rfl
   _ = |(a n - L) + (b n - M)|  := by ring_nf
   _ ≤ |a n - L| + |b n - M|    := abs_add_le _ _
   _ < ε / 2 + ε / 2            := add_lt_add (hNa n (le_of_max_le_left hn))
                                              (hNb n (le_of_max_le_right hn))
   _ = ε                        := add_halves ε

end Solution1

-- Proof 2
-- =======

namespace Solution2

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε / 2) (half_pos hε)
  -- Na : ℕ
  -- hNa : ∀ (n : ℕ), n ≥ Na → |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε / 2) (half_pos hε)
  -- Nb : ℕ
  -- hNb : ∀ (n : ℕ), n ≥ Nb → |b n - M| < ε / 2
  refine ⟨max Na Nb, fun n hn => ?_⟩
  -- n : ℕ
  -- hn : n ≥ max Na Nb
  -- ⊢ |(a + b) n - (L + M)| < ε
  have nNa : n ≥ Na := le_of_max_le_left hn
  specialize hNa n nNa
  -- hNa : |a n - L| < ε / 2
  have nNb : n ≥ Nb := le_of_max_le_right hn
  specialize hNb n nNb
  -- hNb : |b n - M| < ε / 2
  calc |(a + b) n - (L + M)|
     = |(a n + b n) - (L + M)|  := rfl
   _ = |(a n - L) + (b n - M)|  := by ring_nf
   _ ≤ |a n - L| + |b n - M|    := by apply abs_add_le
   _ < ε / 2 + ε / 2            := by linarith [hNa, hNb]
   _ = ε                        := by apply add_halves

end Solution2

-- Proof 3
-- =======

namespace Solution3

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε/2) (by linarith)
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε/2) (by linarith)
  -- Nb : ℕ
  -- hNb : ∀ n ≥ Nb, |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ n ≥ max Na Nb, |(a + b) n - (L + M)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ max Na Nb
  -- ⊢ |(a + b) n - (L + M)| < ε
  have hn₁ : n ≥ Na := le_of_max_le_left hn
  specialize hNa n hn₁
  -- hNa : |a n - L| < ε / 2
  have hn₂ : n ≥ Nb := le_of_max_le_right hn
  specialize hNb n hn₂
  -- hNb : |b n - M| < ε / 2
  calc |(a + b) n - (L + M)|
       = |(a n + b n) - (L + M)|  := by rfl
     _ = |(a n - L) + (b n -  M)| := by {congr; ring}
     _ ≤ |a n - L| + |b n -  M|   := by apply abs_add_le
     _ < ε / 2 + ε / 2            := by linarith
     _ = ε                        := by apply add_halves

end Solution3

-- Proof 4
-- =======

namespace Solution4

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε/2) (by linarith)
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε/2) (by linarith)
  -- Nb : ℕ
  -- hNb : ∀ n ≥ Nb, |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ n ≥ max Na Nb, |(a + b) n - (L + M)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ max Na Nb
  -- ⊢ |(a + b) n - (L + M)| < ε
  obtain ⟨hn₁, hn₂⟩ := max_le_iff.mp hn
  -- hn₁ : n ≥ Na
  -- hn₂ : n ≥ Nb
  calc |(a + b) n - (L + M)|
       = |a n + b n - (L + M)|   := by rfl
     _ = |(a n - L) + (b n - M)| := by { congr; ring }
     _ ≤ |a n - L| + |b n - M|   := by apply abs_add_le
     _ < ε/2 + ε/2               := add_lt_add (hNa n hn₁) (hNb n hn₂)
     _ = ε                       := by simp

end Solution4

-- Proof 5
-- =======

namespace Solution5

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε/2) (by linarith)
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε/2) (by linarith)
  -- Nb : ℕ
  -- hNb : ∀ n ≥ Nb, |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ n ≥ max Na Nb, |(a + b) n - (L + M)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ max Na Nb
  -- ⊢ |(a + b) n - (L + M)| < ε
  obtain ⟨hn₁, hn₂⟩ := max_le_iff.mp hn
  -- hn₁ : Na ≤ n
  -- hn₂ : Nb ≤ n
  have bound₁ : |a n - L| < ε/2 := hNa n hn₁
  have bound₂ : |b n - M| < ε/2 := hNb n hn₂
  calc |(a + b) n - (L + M)|
       = |(a n + b n) - (L + M)| := by rfl
     _ = |(a n - L) + (b n - M)| := by { congr; ring }
     _ ≤ |a n - L| + |b n - M|   := by apply abs_add_le
     _ < ε                       := by linarith

end Solution5

-- Proof 6
-- =======

namespace Solution6

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε Hε
  -- ε : ℝ
  -- Hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε/2) (by linarith)
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε/2) (by linarith)
  -- Nb : ℕ
  -- hNb : ∀ n ≥ Nb, |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ n ≥ max Na Nb, |(a + b) n - (L + M)| < ε
  have h1 : max Na Nb ≥ Na := le_max_left _ _
  have h2 : max Na Nb ≥ Nb := le_max_right _ _
  intros n Hn
  -- n : ℕ
  -- Hn : n ≥ max Na Nb
  -- ⊢ |(a + b) n - (L + M)| < ε
  have h3 : |a n - L| < ε/2 := hNa n (by linarith)
  have h4 : |b n - M| < ε/2 := hNb n (by linarith)
  calc |(a + b) n - (L + M)|
       = |(a n + b n) - (L + M)|   := by rfl
     _ = |(a n - L) + (b n - M)|   := by {congr; ring }
     _ ≤ |(a n - L)| + |(b n - M)| := by apply abs_add_le
     _ < ε/2 + ε/2                 := by linarith
     _ = ε                         := by ring

end Solution6

-- Proof 7
-- =======

namespace Solution7

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hc : ∀ n, c n = a n + b n)
  : SeqLim c (L + M) :=
by
  change ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |c n - (L + M)| < ε
  -- ⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, |c n - (L + M)| < ε
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |c n - (L + M)| < ε
  change ∀ ε₁ > 0, ∃ Na : ℕ, ∀ n ≥ Na, |a n - L| < ε₁ at ha
  -- ha : ∀ ε₁ > 0, ∃ Na, ∀ n ≥ Na, |a n - L| < ε₁
  change ∀ ε₂ > 0, ∃ Nb : ℕ, ∀ n ≥ Nb, |b n - M| < ε₂ at hb
  -- hb : ∀ ε₂ > 0, ∃ Nb, ∀ n ≥ Nb, |b n - M| < ε₂
  specialize ha (ε / 2)
  -- ha : ε / 2 > 0 → ∃ Na, ∀ n ≥ Na, |a n - L| < ε / 2
  specialize hb (ε / 2)
  -- ⊢ ∃ N, ∀ n ≥ N, |c n - (L + M)| < ε
  have hε2 : 0 < ε / 2 := by linarith [hε]
  specialize ha hε2
  -- ha : ∃ Na, ∀ n ≥ Na, |a n - L| < ε / 2
  specialize hb hε2
  -- hb : ∃ Nb, ∀ n ≥ Nb, |b n - M| < ε / 2
  choose Na hNa using ha
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε / 2
  choose Nb hNb using hb
  -- Nb : ℕ
  -- hNb : ∀ n ≥ Nb, |b n - M| < ε / 2
  use Na + Nb
  -- ⊢ ∀ n ≥ Na + Nb, |c n - (L + M)| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ Na + Nb
  -- ⊢ |c n - (L + M)| < ε
  specialize hc n
  -- hc : c n = a n + b n
  rewrite [hc]
  -- ⊢ |a n + b n - (L + M)| < ε
  have h1 : a n + b n - (L + M) =
    (a n - L) + (b n - M) := by ring_nf
  rewrite [h1]
  -- ⊢ |a n - L + (b n - M)| < ε
  specialize hNa n
  -- hNa : n ≥ Na → |a n - L| < ε / 2
  specialize hNb n
  -- hNb : n ≥ Nb → |b n - M| < ε / 2
  have h2 : Na ≤ n := by linarith
  have h3 : Nb ≤ n := by linarith
  specialize hNa h2
  -- hNa : |a n - L| < ε / 2
  specialize hNb h3
  -- hNb : |b n - M| < ε / 2
  have h4 : |a n - L + (b n - M)| ≤
    |a n - L| + |(b n - M)| := by apply abs_add_le
  linarith [abs_add_le (a n - L) (b n - M)]

end Solution7

-- Proof 8
-- =======

namespace Solution8

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε/2) (by linarith)
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε/2) (by linarith)
  -- Nb : ℕ
  -- hNb : ∀ n ≥ Nb, |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ n ≥ max Na Nb, |(a + b) n - (L + M)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ max Na Nb
  -- ⊢ |(a + b) n - (L + M)| < ε
  specialize hNa n (le_of_max_le_left hn)
  -- hNa : |a n - L| < ε / 2
  specialize hNb n (le_of_max_le_right hn)
  -- hNb : |b n - M| < ε / 2
  simp
  -- ⊢ |a n + b n - (L + M)| < ε
  grind

end Solution8

-- Proof 9
-- =======

namespace Solution9

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(a + b) n - (L + M)| < ε
  obtain ⟨Na, hNa⟩ := ha (ε / 2) (by grind)
  -- Na : ℕ
  -- hNa : ∀ (n : ℕ), n ≥ Na → |a n - L| < ε / 2
  obtain ⟨Nb, hNb⟩ := hb (ε / 2) (by grind)
  -- Nb : ℕ
  -- hNb : ∀ (n : ℕ), n ≥ Nb → |b n - M| < ε / 2
  use max Na Nb
  -- ⊢ ∀ (n : ℕ), n ≥ max Na Nb → |(s + t) n - (L + M)| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |(a + b) n - (L + M)| < ε
  calc |(a + b) n - (L + M)|
     = |(a n + b n) - (L + M)|  := rfl
   _ = |(a n - L) + (b n - M)|  := by grind
   _ ≤ |a n - L| + |b n - M|    := by grind
   _ < ε / 2 + ε / 2            := by grind
   _ = ε                        := by grind

end Solution9

-- Lemmas used
-- ===========

variable (x y z z' : ℝ)
#check (abs_add_le x y : |x + y| ≤ |x| + |y|)
#check (add_halves x : x / 2 + x / 2 = x)
#check (add_lt_add : x < y → z < z' → x + z < y + z')
#check (half_pos : x > 0 → x / 2 > 0)
#check (le_max_left x y : x ≤ max x y)
#check (le_max_right x y : y ≤ max x y)
#check (le_of_max_le_left : max x y ≤ z → x ≤ z)
#check (le_of_max_le_right : max x y ≤ z → y ≤ z)
#check (max_le_iff : max x y ≤ z ↔ x ≤ z ∧ y ≤ z)

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