Skip to main content

If a converges to L, then (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1]

Also available in:

Español

Prove that if the sequence \(a\) converges to \(L\), then \[ (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1] \]

To do so, complete the following Lean 4 theory:

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

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

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

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
by
  sorry

1. Proof in natural language

Since \(a\) converges to \(L\), there exists an \(N ∈ ℕ\) such that \[ (∀ n ≥ N) |aₙ - L| < 1 \tag{1} \] We show that \[ (∀ n ≥ N) [aₙ ≥ L - 1] \] Indeed, let \(n ≥ N\). By (1), \[ |aₙ - L| < 1 \] Hence, \begin{align} &-1 < aₙ - L ∧ aₙ - L < 1 \newline &\Longrightarrow -1 < aₙ - L \newline &\Longrightarrow aₙ ≥ L - 1 \end{align}

2. Proofs in Lean 4

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

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

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

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

variable (x : ℝ)

lemma L1
  (h : -1 < x)
  : 0 ≤ x + 1 :=
by
  have h1 : -1 + 1 < x + 1 := (add_lt_add_iff_right 1).mpr h
  have h2 : 0 < x + 1 := neg_lt_iff_pos_add.mp h
  exact le_of_lt h2

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
by
  obtain ⟨N, hN⟩ := ha 1 one_pos
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < 1
  use N
  -- ⊢ ∀ n ≥ N, a n ≥ L - 1
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ a n ≥ L - 1
  have h1 : |a n - L| < 1 := hN n hn
  have h2 : -1 < a n - L ∧ a n - L < 1 := abs_lt.mp h1
  have h3 : -1 < a n - L := h2.1
  rw [ge_iff_le, ← sub_nonneg]
  -- ⊢ 0 ≤ a n - (L - 1)
  calc 0
     _ ≤ (a n - L) + 1 := L1 (a n - L) h3
     _ = a n - (L - 1) := sub_add (a n) L 1

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

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
by
  obtain ⟨N, hN⟩ := ha 1 one_pos
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < 1
  use N
  -- ⊢ ∀ n ≥ N, a n ≥ L - 1
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ a n ≥ L - 1
  have h1 : -1 < a n - L := (abs_lt.mp (hN n hn)).1
  have h2 : a n - (L - 1) = (a n - L) + 1 := (sub_add (a n) L 1).symm
  rw [ge_iff_le, ← sub_nonneg]
  -- ⊢ 0 ≤ a n - (L - 1)
  rw [h2]
  -- ⊢ 0 ≤ a n - L + 1
  exact neg_le_iff_add_nonneg.mp (le_of_lt h1)

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

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
by
  obtain ⟨N, hN⟩ := ha 1 one_pos
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < 1
  use N
  -- ⊢ ∀ n ≥ N, a n ≥ L - 1
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ a n ≥ L - 1
  have h1 : -1 < a n - L := (abs_lt.mp (hN n hn)).1
  rw [ge_iff_le, ← sub_nonneg]
  -- ⊢ 0 ≤ a n - (L - 1)
  calc 0
     _ ≤ (a n - L) + 1 := by grind
     _ = a n - (L - 1) := by grind

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

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
by
  obtain ⟨N, hN⟩ := ha 1 one_pos
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < 1
  use N
  -- ⊢ ∀ n ≥ N, a n ≥ L - 1
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ a n ≥ L - 1
  have : -1 < a n - L := (abs_lt.mp (hN n hn)).1
  linarith

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

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
by
  obtain ⟨N, hN⟩ := ha 1 (by grind)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < 1
  refine ⟨N, fun n hn => ?_⟩
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ a n ≥ L - 1
  grind

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

example
  (ha : SeqLim a L) :
  ∃ N, ∀ n ≥ N, a n ≥ L - 1 :=
let ⟨N, hN⟩ := ha 1 (by grind)
⟨N, fun n hn => by grind⟩

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

variable (x y z : ℝ)
#check (abs_lt : |x| < y ↔ -y < x ∧ x < y)
#check (add_lt_add_iff_right x : y + x < z + x ↔ y < z)
#check (ge_iff_le : x ≥ y ↔ y ≤ x)
#check (le_of_lt : x < y → x ≤ y)
#check (neg_le_iff_add_nonneg : -x ≤ y ↔ 0 ≤ y + x)
#check (neg_lt_iff_pos_add : -x < y ↔ 0 < y + x)
#check (one_pos : 0 < 1)
#check (sub_add x y z : x - y + z = x - (y - z))
#check (sub_nonneg : 0 ≤ x - y ↔ y ≤ x)

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