Skip to main content

Challenge 6: If aₙ and cₙ converge to L and aₙ ≤ bₙ ≤ cₙ for all n, then bₙ converges to L

Also available in:

Español

Prove the squeeze theorem; that is, if \(a_n\) and \(c_n\) converge to \(L\) and \(a_n ≤ b_n \leq c_n\) for all \(n\), then \(b_n\) converges to \(L\).

To do so, complete the following Lean 4 theory:

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

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

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

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L := by
  sorry

1. Proof in natural language

Let \(ε > 0\). We have to prove that there exists an N such that \[ ∀ n ≥ N, |bₙ - L| < ε \tag{1} \]

Since \(a\) and \(c\) converge to \(L\), there exist \(N_1\) and \(N_2\) such that \[ ∀ n ≥ N_1, |a_n - L| < ε \tag{2} \] \[ ∀ n ≥ N_2, |c_n - L| < ε \tag{3} \] Let \[ N = \max(N_1, N_2) \tag{4} \] To prove (1), let \(n ≥ N\). By (4), we have \[ n ≥ N_1 \] \[ n ≥ N_2 \] Hence, using (2) and (3), we have \begin{array}{l} |a_n - L| < ε \\ |c_n - L| < ε \end{array} from which it follows that \[ - ε < a_n - L < ε \tag{5} \] \[ - ε < c_n - L < ε \tag{6} \] Hence, \begin{array}{lll} -ε &< a_n - L &&\text{[by (5)]} \\ &≤ b_n - L &&\text{[by the hypothesis on b]} \\ &≤ c_n - L &&\text{[by the hypothesis on b]} \\ &< ε &&\text{[by (6)]} \end{array} Therefore, \[ -ε < b_n - L < ε \] and, finally, \[ |b_n - L| < ε \]

2. Proofs in Lean 4

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

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

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

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

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - L| < ε
  obtain ⟨Na, hNa⟩ := ha ε hε
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε
  obtain ⟨Nc, hNc⟩ := hc ε hε
  -- Nc : ℕ
  -- hNc : ∀ n ≥ Nc, |c n - L| < ε
  exact ⟨max Na Nc, by grind⟩

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

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - L| < ε
  have ha : ∃ N, ∀ n ≥ N, |a n - L| < ε := ha ε hε
  have hb : ∃ N, ∀ n ≥ N, |c n - L| < ε := hc ε hε
  obtain ⟨Na, hNa⟩ := ha
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε
  obtain ⟨Nc, hNc⟩ := hb
  -- Nc : ℕ
  -- hNc : ∀ n ≥ Nc, |c n - L| < ε
  use max Na Nc
  -- ⊢ ∀ n ≥ max Na Nc, |b n - L| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ max Na Nc
  -- ⊢ |b n - L| < ε
  rewrite [abs_lt]
  -- ⊢ -ε < b n - L ∧ b n - L < ε
  constructor
  · -- ⊢ -ε < b n - L
    calc -ε
       < a n - L := by grind
     _ ≤ b n - L := by grind
  · -- ⊢ b n - L < ε
    calc b n - L
       ≤ c n - L := by grind
     _ < ε       := by grind

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

example
    (ha : SeqLim a L)
    (hc : SeqLim c L)
    (hab : ∀ n, a n ≤ b n)
    (hbc : ∀ n, b n ≤ c n) :
    SeqLim b L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - L| < ε
  obtain ⟨Na, hNa⟩ := ha ε hε
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε
  obtain ⟨Nc, hNc⟩ := hc ε hε
  -- Nc : ℕ
  -- hNc : ∀ n ≥ Nc, |c n - L| < ε
  refine ⟨max Na Nc, fun n hn => ?_⟩
  -- n : ℕ
  -- hn : n ≥ max Na Nc
  -- ⊢ |b n - L| < ε
  have hna := hNa n (le_of_max_le_left hn)
  have hnc := hNc n (le_of_max_le_right hn)
  rw [abs_lt] at hna hnc ⊢
  -- hna : -ε < a n - L ∧ a n - L < ε
  -- hnc : -ε < c n - L ∧ c n - L < ε
  -- ⊢ -ε < b n - L ∧ b n - L < ε
  exact ⟨by linarith [hab n], by linarith [hbc n]⟩

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

example
    (ha : SeqLim a L)
    (hc : SeqLim c L)
    (hab : ∀ n, a n ≤ b n)
    (hbc : ∀ n, b n ≤ c n)
    : SeqLim b L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - L| < ε
  obtain ⟨Na, hNa⟩ := ha ε hε
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε
  obtain ⟨Nc, hNc⟩ := hc ε hε
  -- Nc : ℕ
  -- hNc : ∀ n ≥ Nc, |c n - L| < ε
  refine ⟨max Na Nc, fun n hn => ?_⟩
  -- n : ℕ
  -- hn : n ≥ max Na Nc
  -- ⊢ |b n - L| < ε
  have hna := hNa n (le_of_max_le_left hn)
  have hnc := hNc n (le_of_max_le_right hn)
  rw [abs_lt] at hna hnc ⊢
  -- hna : -ε < a n - L ∧ a n - L < ε
  -- hnc : -ε < c n - L ∧ c n - L < ε
  -- ⊢ -ε < b n - L ∧ b n - L < ε
  refine ⟨?_, ?_⟩
  · -- ⊢ -ε < b n - L
    calc -ε
         < a n - L := hna.1
       _ ≤ b n - L := by linarith [hab n]
  · calc b n - L
         ≤ c n - L := by linarith [hbc n]
       _ < ε       := hnc.2

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

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - L| < ε
  have ha : ∃ N, ∀ n ≥ N, |a n - L| < ε := ha ε hε
  have hb : ∃ N, ∀ n ≥ N, |c n - L| < ε := hc ε hε
  obtain ⟨Na, hNa⟩ := ha
  -- Na : ℕ
  -- hNa : ∀ n ≥ Na, |a n - L| < ε
  obtain ⟨Nc, hNc⟩ := hb
  -- Nc : ℕ
  -- hNc : ∀ n ≥ Nc, |c n - L| < ε
  use max Na Nc
  -- ⊢ ∀ n ≥ max Na Nc, |b n - L| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ max Na Nc
  -- ⊢ |b n - L| < ε
  have hna : Na ≤ n := le_of_max_le_left hn
  have hnc : Nc ≤ n := le_of_max_le_right hn
  have hNa : |a n - L| < ε := hNa n hna
  have hNc : |c n - L| < ε := hNc n hnc
  rewrite [abs_lt] at hNa
  -- hNa : -ε < a n - L ∧ a n - L < ε
  rewrite [abs_lt] at hNc
  -- hNc : -ε < c n - L ∧ c n - L < ε
  rewrite [abs_lt]
  -- ⊢ -ε < b n - L ∧ b n - L < ε
  constructor
  · -- ⊢ -ε < b n - L
    calc -ε
       < a n - L := hNa.1
     _ ≤ b n - L := sub_le_sub_right (hab n) L
  · -- ⊢ b n - L < ε
    calc b n - L
       ≤ c n - L := sub_le_sub_right (hbc n) L
     _ < ε       := hNc.2

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