Skip to main content

Posts about Lean 4 Challenges (old posts, page 1)

Subcategories:

RSS feed (Lean 4 Challenges, en)

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…

Challenge 7: The composition of injective functions is injective

Lean 4 Challenges/Foundations/Functions

Prove that the composition of injective functions is injective.

To do so, complete the following Lean 4 theory:

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by sorry

Read more…

Challenge 6: If aₙ and cₙ converge to L and aₙ ≤ bₙ ≤ cₙ for all n, then bₙ converges to L

Lean 4 Challenges/Analysis/Limits

Prove the squeeze theorem; that is, if \(a_n\) and \(c_n\) converge to \(L\) and \(a_n ≤ b_n \leq c_n\) for all \(n\), then \(b_n\) converges to \(L\).

To do so, complete the following Lean 4 theory:

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

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

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

example
  (ha : SeqLim a L)
  (hc : SeqLim c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : SeqLim b L := by
  sorry

Read more…

Challenge 5: 5²ⁿ - 2³ⁿ is divisible by 17

Lean 4 Challenges/Number theory/Induction

Prove in Lean 4 that 5²ⁿ - 2³ⁿ is divisible by 17 for every natural number n.

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

variable (n : ℕ)

open Nat

example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by
  sorry

Read more…