Skip to main content

Challenge 10: If aₙ → L with L ≠ 0, then |aₙ| ≥ |L|/2 eventually

Also available in:

Español

Prove that if a sequence converges to a nonzero limit, then its terms are eventually bounded below by half the absolute value of the limit; that is, if a sequence \(a_n\) converges to \(L\) with \(L ≠ 0\), then there exists \(k\) such that for all \(n ≥ k\) we have \(|aₙ| ≥ \dfrac{|L|}{2}\).

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 : SeqLim a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 :=
by sorry

1. Proof in natural language

Since \(L ≠ 0\), we have \[ \dfrac{|L|}{2} > 0 \] and, as \(a\) converges to \(L\), there exists a \(k\) such that \[ ∀ n ≥ k, |aₙ - L| < \dfrac{|L|}{2} \tag{1} \] We show that \[ ∀ n ≥ k, |aₙ| ≥ \dfrac{|L|}{2} \] Indeed, let \(n ≥ k\). Then, by (1), \[ |aₙ - L| < \dfrac{|L|}{2} \tag{2} \] Moreover, \[ \begin{array}{llll} |L| &= |aₙ + (L - aₙ)| \\ &≤ |aₙ| + |L - aₙ| \\ &= |aₙ| + |-(aₙ - L)| \\ &= |aₙ| + |aₙ - L| \\ &≤ |aₙ| + \dfrac{|L|}{2} &&\text{[by (2)]} \end{array} \] Hence, \[ |L| ≤ |aₙ| + \dfrac{|L|}{2} \] and, therefore, \[ |aₙ| ≥ \dfrac{|L|}{2} \]

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 : SeqLim a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 :=
by
  obtain ⟨k, hk⟩ := ha (|L| / 2) (by grind)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < |L| / 2
  use k
  -- ⊢ ∀ n ≥ k, |L| / 2 ≤ |a n|
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |L| / 2 ≤ |a n|
  grind

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

example
  (ha : SeqLim a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k,  |a n| ≥ |L| / 2 :=
by
  obtain ⟨k, hk⟩ := ha (|L| / 2) (by grind)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < |L| / 2
  use k
  -- ⊢ ∀ n ≥ k, |L| / 2 ≤ |a n|
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |L| / 2 ≤ |a n|
  have h3 : |a n - L| < |L| / 2 := hk n hn
  have h4 : |L| ≤ |a n| + |L| / 2 := by
    calc |L|
         = |a n + (L - a n)|    := by grind
       _ ≤ |a n| + |L - a n|    := by grind
       _ = |a n| + |-(a n - L)| := by grind
       _ = |a n| + |a n - L|    := by grind
       _ ≤ |a n| + |L| / 2      := by grind
  grind

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

example
  (ha : SeqLim a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 :=
by
  obtain ⟨k, hk⟩ := ha (|L| / 2) (by positivity)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < |L| / 2
  use k
  -- ⊢ ∀ n ≥ k, |L| / 2 ≤ |a n|
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |L| / 2 ≤ |a n|
  have h3 : |a n - L| < |L| / 2 := hk n hn
  have h4 : |L| ≤ |a n| + |L| / 2 := by
    calc |L|
         = |a n + (L - a n)|    := by ring_nf
       _ ≤ |a n| + |L - a n|    := abs_add_le (a n) (L - a n)
       _ = |a n| + |-(a n - L)| := by ring_nf
       _ = |a n| + |a n - L|    := by congr 1 ; exact abs_neg (a n - L)
       _ ≤ |a n| + |L| / 2      := by gcongr
  linarith [h4]

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

example
  (ha : SeqLim a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 :=
by
  have h1 : 0 < |L| := abs_pos.mpr hL
  have h2 : 0 < |L| / 2 := half_pos h1
  obtain ⟨k, hk⟩ := ha (|L| / 2) h2
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < |L| / 2
  use k
  -- ⊢ ∀ n ≥ k, |L| / 2 ≤ |a n|
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |L| / 2 ≤ |a n|
  have h3 : |a n - L| < |L| / 2 := hk n hn
  have h4 : |L| ≤ |a n| + |L| / 2 := by calc
    |L| = |a n + (L - a n)|    := by ring_nf
      _ ≤ |a n| + |L - a n|    := abs_add_le (a n) (L - a n)
      _ = |a n| + |-(a n - L)| := congrArg (|a n| + |·|) (neg_sub (a n) L).symm
      _ = |a n| + |a n - L|    := congrArg (|a n| + ·) (abs_neg (a n - L))
      _ ≤ |a n| + |L| / 2      := add_le_add_right (le_of_lt h3) |a n|
  calc |L| / 2
       = |L| - |L| / 2 := (sub_half |L|).symm
     _ ≤ |a n|         := tsub_le_iff_right.mpr h4

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

lemma exists_half_abs_le_abs_of_seqLim_of_ne_zero
  (ha : SeqLim a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 :=
by
  obtain ⟨k, hk⟩ := ha (|L| / 2) (by grind)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < |L| / 2
  refine ⟨k, fun _ _ => by grind⟩

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

variable (x y z : ℝ)
#check (abs_add_le x y : |x + y| ≤ |x| + |y|)
#check (abs_neg x : |(-x)| = |x|)
#check (abs_pos : 0 < |x| ↔ x ≠ 0)
#check (add_le_add_right : y ≤ z → ∀ x, x + y ≤ x + z)
#check (half_pos : 0 < x → 0 < x / 2)
#check (neg_sub x y : -(x - y) = y - x)
#check (sub_half x : x - x / 2 = x / 2)
#check (tsub_le_iff_right : x - y ≤ z ↔ x ≤ z + y)

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