Skip to main content

Challenge 23: The constant sequence aₙ = L converges to L

Also available in:

Español

Prove that the constant sequence \(a_{n} = L\) converges to \(L\).

To do so, complete the following theory:

import Mathlib.Tactic

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

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by sorry

1. Proof in natural language

We have to prove that for every \(\varepsilon \in ℝ\) with \(\varepsilon > 0\), there exists a \(k \in ℕ\) such that \[ ∀ n ≥ k, |a_n - L| < \varepsilon \] We take \(k = 0\). For every \(n ≥ k\), since \(a_n = L\), we have \[ \begin{array}{ll} |a_n - L| &= |L - L| \\ &= |0| \\ &= 0 \\ &< \varepsilon \\ \end{array} \]

2. Proofs in Lean 4

import Mathlib.Tactic

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

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

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  grind

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  refine ⟨0, by grind⟩

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
fun _ _ => ⟨0, by grind⟩

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := by grind
   _ = 0          := by grind
   _ < ε          := by grind

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := by rw [h n]
   _ = 0          := by norm_num
   _ < ε          := hε

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := by rw [h]
   _ = |0|        := by rw [sub_self L]
   _ = 0          := abs_zero
   _ < ε          := hε

-- Proof 7
-- =======

theorem SeqLim_const
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := congrArg (|· - L|) (h n)
   _ = |0|        := congrArg abs (sub_self L)
   _ = 0          := abs_zero
   _ < ε          := hε

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

-- #check (abs_zero : |(0 : ℝ)| = 0)
-- #check (sub_self L : L - L = 0)

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