Skip to main content

Challenge 17: Convergent sequences are bounded

Lean 4 Challenges/Analysis/Limits

Prove that if a sequence \(a_n\) is convergent, then \(a_n\) is bounded; that is, there exists an \(M ∈ ℝ\) such that for every \(n ∈ ℕ\), \(|a_n| ≤ M\).

To do so, complete the following Lean 4 theory:

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

open Finset

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

def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

def SeqBdd (a : ℕ → ℝ) : Prop :=
  ∃ M, ∀ n, |a n| ≤ M

variable (a : ℕ → ℝ)

example
  (ha : SeqConv a)
  : SeqBdd a :=
by sorry

Read more…

Challenge 13: Reverse triangle inequality: ||x| - |y|| ≤ |x - y|

Lean 4 Challenges/Analysis/Real numbers

Prove the reverse triangle inequality; that is, that for all real numbers \(x\) and \(y\), the following relation holds: \[ ||x| - |y|| ≤ |x - y| \]

To do so, complete the following Lean 4 theory:

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

variable (x y : ℝ)

example : |(|x| - |y|)| ≤ |x - y| :=
by sorry

Read more…

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

Lean 4 Challenges/Analysis/Limits

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

Read more…

Challenge 11: If aₙ converges to L, then |aₙ| converges to |L|

Lean 4 Challenges/Analysis/Limits

Prove that if the sequence \(a_n\) converges to \(L\), then \(|a_n|\) converges to \(|L|\).

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 : ℝ}

example
  (ha : SeqLim a L)
  (hb : ∀ n, b n = |a n|)
  : SeqLim b |L| :=
by sorry

Read more…

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

Lean 4 Challenges/Analysis/Limits

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

Read more…

Challenge 9: Uniqueness of the limit

Lean 4 Challenges/Analysis/Limits

This week's challenge consists of proving in Lean 4 that if a sequence \(aₙ\) converges to both \(L\) and \(M\), then \(L = M\).

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 M : ℝ}

example
  (hL : SeqLim a L)
  (hM : SeqLim a M)
  : L = M :=
by sorry

Read more…

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

Lean 4 Challenges/Analysis/Limits

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

Read more…