Skip to main content

Challenge 12: If aₙ → L, bₙ → M and L < M, then eventually aₙ < bₙ

Also available in:

Español

Prove that if the sequences \(a_n\) and \(b_n\) converge to \(L\) and \(M\), respectively, with \(L < M\), then eventually \(a_n < b_n\); that is, there exists \(k ∈ \mathbb{N}\) such that, for all \(n ≥ k\), \(a_n < b_n\).

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 : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by sorry

1. Proof in natural language

Let \[ \varepsilon = \dfrac{M - L}{2} \tag{1} \]

Since \(L < M\), we have \(\varepsilon > 0\). And, using the convergence of \(a_n\) and \(b_n\), there exist \(k_1\) and \(k_2\) such that \[ \forall n ≥ k_1, |a_n - L| < \varepsilon \tag{2} \] \[ \forall n ≥ k_2, |b_n - M| < \varepsilon \tag{3} \] Let \[ k = \max(k_1, k_2) \tag{4} \] We show that \[ \forall n \geq k, a_n < b_n \] To do so, let \(n ∈ \mathbb{N}\) be such that \[ n \geq k \tag{5} \] Then, by (4) and (5), we have \[ n \geq k_1 \] Hence, by (2), we have \[ |a_n - L| < \varepsilon \] and, consequently, \[ a_n - L < \varepsilon \tag{6} \]

Also, by (4) and (5), we have \[ n \geq k_2 \] Hence, by (3), we have \[ |b_n - M| < \varepsilon \] and, consequently, \[ -\varepsilon < b_n - M \tag{7} \]

Finally, \[ \begin{array}{llll} a_n &< \varepsilon + L &&\text{[by (6)]} \\ &= \dfrac{M - L}{2} + L &&\text{[by (1)]} \\ &= \dfrac{L + M}{2} \\ &= -\left(\dfrac{M - L}{2}\right) + M \\ &= -\varepsilon + M &&\text{[by (1)]} \\ &< b_n &&\text{[by (7)]} \\ \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 b : ℕ → ℝ}
variable {L M : ℝ}

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

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by grind)
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε (by grind)
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  use max k1 k2
  -- ⊢ ∀ n ≥ max k1 k2, a n < b n
  grind

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

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by grind)
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε (by grind)
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  use max k1 k2
  -- ⊢ ∀ n ≥ max k1 k2, a n < b n
  intro n hn
  -- n : ℕ
  -- hn : n ≥ max k1 k2
  -- ⊢ a n < b n
  calc
    a n
    < ε + L              := by grind
  _ = (M - L) / 2 + L    := by grind
  _ = (L + M) / 2        := by grind
  _ = -((M - L) / 2) + M := by grind
  _ = -ε + M             := by grind
  _ < b n                := by grind

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

example
    (ha : SeqLim a L)
    (hb : SeqLim b M)
    (hLM : L < M) :
    ∃ k, ∀ n ≥ k, a n < b n := by
  set ε := (M - L) / 2 with ε_def
  -- ε_def : ε = (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by positivity)
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε (by positivity)
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  set k := max k1 k2
  use k
  -- ⊢ ∀ n ≥ k, a n < b n
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ a n < b n
  have h1 : n ≥ k1 := le_of_max_le_left hn
  have h2 : |a n - L| < ε := hk1 n h1
  have h3 : a n - L < ε := lt_of_abs_lt h2
  have h4 : n ≥ k2 := le_of_max_le_right hn
  have h5 : |b n - M| < ε := hk2 n h4
  have h6 : -ε < b n - M := neg_lt_of_abs_lt h5
  calc
    a n
    < ε + L              := lt_add_of_tsub_lt_right h3
  _ = (M - L) / 2 + L    := by rw [ε_def]
  _ = (L + M) / 2        := by ring
  _ = -((M - L) / 2) + M := by ring
  _ = -ε + M             := by rw [ε_def]
  _ < b n                := lt_tsub_iff_right.mp h6

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

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2 with ε_def
  -- ε_def : ε = (M - L) / 2
  have hε : ε > 0 := half_pos (sub_pos_of_lt hLM)
  obtain ⟨k1, hk1⟩ := ha ε hε
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε hε
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  set k := max k1 k2
  use k
  -- ⊢ ∀ n ≥ k, a n < b n
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ a n < b n
  have h1 : n ≥ k1 := le_of_max_le_left hn
  have h2 : |a n - L| < ε := hk1 n h1
  have h3 : a n - L < ε := lt_of_abs_lt h2
  have h4 : n ≥ k2 := le_of_max_le_right hn
  have h5 : |b n - M| < ε := hk2 n h4
  have h6 : -ε < b n - M := neg_lt_of_abs_lt h5
  calc
    a n
    < ε + L              := lt_add_of_tsub_lt_right h3
  _ = (M - L) / 2 + L    := congrArg (· + L) ε_def
  _ = (L + M) / 2        := by ring
  _ = -((M - L) / 2) + M := by ring
  _ = -ε + M             := congrArg (-· + M) ε_def
  _ < b n                := lt_tsub_iff_right.mp h6

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

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by grind)
  obtain ⟨k2, hk2⟩ := hb ε (by grind)
  exact ⟨max k1 k2, fun _ _ => by grind⟩

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