Skip to main content

Challenge 8: Sequences with infinitely many large terms do not converge to small limits

Also available in:

Español

Prove that a sequence with infinitely many terms whose absolute value is greater than 10 cannot converge to a limit whose absolute value is less than 5.

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

example
  (ha : ∀ k, ∃ n ≥ k, |a n| > 10)
  : ¬ ∃ L, SeqLim a L ∧ |L| < 5 :=
by sorry

1. Proof in natural language

To prove the negation, we assume that there exists \(L ∈ ℝ\) such that \(a_n\) converges to \(L\) and \[ |L| < 5 \tag{1} \] and we derive a contradiction.

By the definition of limit, using \(ε = 5 > 0\), there exists \(k ∈ ℕ\) such that \[ ∀ n ≥ k, |a_n − L| < 5 \tag{2} \]

By the hypothesis on the sequence, for this same \(k\) there exists \(n ∈ ℕ\) such that the following two relations hold: \[ n ≥ k \tag{3} \] \[ |a_n| > 10 \tag{4} \] From (2) and (3) we have \[ |a_n − L| < 5 \tag{5} \]

To obtain a contradiction it suffices to prove that \(10 < 10\), which is proved as follows: \[ \begin{array}{llll} 10 &< |a_n| &&\text{[by (4)]} \\ &= |(a_n − L) + L| \\ &≤ |a_n − L| + |L| &&\text{[by the triangle inequality]} \\ &< 5 + 5 &&\text{[by (5) and (1)]} \\ &= 10 \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 : ℕ → ℝ}
variable {L : ℝ}

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

example
  (ha : ∀ k, ∃ n ≥ k, |a n| > 10)
  : ¬ ∃ L, SeqLim a L ∧ |L| < 5 :=
by
  intro ⟨L, hL1, hL2⟩
  -- L : ℝ
  -- hL1 : SeqLim a L
  -- hL2 : |L| < 5
  -- ⊢ False
  obtain ⟨k, hk⟩ := hL1 5 (by norm_num)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < 5
  obtain ⟨n, hn1, hn2⟩ := ha k
  -- n : ℕ
  -- hn1 : n ≥ k
  -- hn2 : |a n| > 10
  grind

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

example
  (ha : ∀ k, ∃ n ≥ k, |a n| > 10)
  : ¬ ∃ L, SeqLim a L ∧ |L| < 5 :=
by
  intro ⟨L, hL1, hL2⟩
  -- L : ℝ
  -- hL1 : SeqLim a L
  -- hL2 : |L| < 5
  -- ⊢ False
  obtain ⟨k, hk⟩ := hL1 5 (by norm_num)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < 5
  obtain ⟨n, hn1, hn2⟩ := ha k
  -- n : ℕ
  -- hn1 : n ≥ k
  -- hn2 : |a n| > 10
  apply lt_irrefl (10 : ℝ)
  -- ⊢ 10 < 10
  calc 10 < |a n|        := hn2
     _ = |(a n - L) + L| := by grind
     _ ≤ |a n - L| + |L| := by grind
     _ < 5 + 5           := by grind
     _ = 10              := by grind

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

example
  (ha : ∀ k, ∃ n ≥ k, |a n| > 10)
  : ¬ ∃ L, SeqLim a L ∧ |L| < 5 :=
by
  intro ⟨L, hL1, hL2⟩
  -- L : ℝ
  -- hL1 : SeqLim a L
  -- hL2 : |L| < 5
  -- ⊢ False
  obtain ⟨k, hk⟩ := hL1 5 (by positivity)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < 5
  obtain ⟨n, hn1, hn2⟩ := ha k
  -- n : ℕ
  -- hn1 : n ≥ k
  -- hn2 : |a n| > 10
  apply lt_irrefl (10 : ℝ)
  -- ⊢ 10 < 10
  have h5 : |a n - L| < 5 := hk n hn1
  calc 10 < |a n|         := hn2
     _ = |(a n - L) + L|  := congrArg abs (sub_add_cancel (a n) L).symm
     _ ≤ |a n - L| + |L|  := abs_add_le (a n - L) L
     _ < 5 + 5            := add_lt_add h5 hL2
     _ = 10               := by norm_num

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

variable (a b c d : ℝ)

#check (abs_add_le a b : |a + b| ≤ |a| + |b|)
#check (add_lt_add : a < b → c < d → a + c < b + d)
#check (lt_irrefl a : ¬a < a)
#check (sub_add_cancel a b : (a - b) + b = a)

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