Skip to main content

Posts about Lean4Challenge

RSS feed (Lean4Challenge, en)

Canal RSS (RetoLean4, es)

Also available in:

Español (RetoLean4)

Challenge 26: Product of a sequence with limit zero and a bounded sequence

Lean 4 Challenges/Analysis/Limits

Prove that if the sequence \(a_n\) converges to \(0\) and the sequence \(b_n\) is bounded (not necessarily convergent), then the sequence \(a_n·b_n\) converges to \(0\).

To do so, complete the following theory

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

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

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

variable (a b : ℕ → ℝ)

example
  (ha : SeqLim a 0)
  (hb : SeqBdd b)
  : SeqLim (a * b) 0 :=
by sorry

Collaborative solutions

How can you post your solution?

  • 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
```
  • During the week you will be able to compare your approach with those of other participants. The official solution will be published Monday 9 November 2026.

Challenge 25: If the interleaving of two sequences converges to L, then both converge to L

Lean 4 Challenges/Analysis/Limits

Suppose that the sequence \(c_n\) is an interleaving of the sequences \(a_n\) and \(b_n\); that is, that \[ (c_0, c_1, c_2, \dots) = (a_0, b_0, a_1, b_1, a_2, b_2, \dots) \]

Prove that if \(c_n\) converges to \(L\), then \(a_n\) and \(b_n\) converge to \(L\).

To do so, complete the following theory

import Mathlib.Tactic

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

example
  (hc : ∀ n, c n = if Even n
                   then a (n / 2)
                   else b ((n - 1) / 2))
  (hL : SeqLim c L)
  : SeqLim a L ∧ SeqLim b L :=
by sorry

Read more…

Challenge 24: The sequence 1, -1, 1, -1,... is not convergent (2nd version)

Lean 4 Challenges/Analysis/Limits

Using Challenge 22 (which states that if a sequence has two subsequences that converge to different limits, then the sequence is not convergent), prove that the sequence defined by 1, -1, 1, -1, ... is not convergent.

To do so, complete the following theory:

import Mathlib.Tactic

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

-- The sequence a is convergent
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b is a subsequence of a.
def Subseq (b a : ℕ → ℝ) : Prop :=
  ∃ φ, IsExtraction φ ∧ b = a ∘ φ

variable {a : ℕ → ℝ}

example
  (ha : ∀ n, a n = (-1)^n)
  : ¬SeqConv a :=
by sorry

Read more…

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

Lean 4 Challenges/Analysis/Limits

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

Read more…

Challenge 22: Subsequences with different limits imply non-convergence

Lean 4 Challenges/Analysis/Limits

Prove that if a sequence has two subsequences with different limits, then the sequence is not convergent.

To do so, complete the following theory:

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

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

-- The sequence a is convergent
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b is a subsequence of a.
def Subseq (b a : ℕ → ℝ) : Prop :=
  ∃ φ, IsExtraction φ ∧ b = a ∘ φ

variable {a b₁ b₂ : ℕ → ℝ}
variable {L L₁ L₂ : ℝ}

example
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SeqConv a :=
by sorry

Read more…

Challenge 21: Subsequences have the same limit as the sequence

Lean 4 Challenges/Analysis/Limits

A subsequence is obtained by applying an extraction function to the original sequence; that is, a strictly increasing function \(φ : ℕ \to ℕ\). For example, the subsequence \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] is obtained with the extraction function \(\varphi\) defined by \(\varphi(n) = 2n\).

The previous definitions are formalized in Lean 4 as:

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) :=
  StrictMono φ

-- v is a subsequence of u.
def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

-- a is the limit of u.
def SeqLim (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

Prove that every subsequence of a convergent sequence converges to the same limit as the sequence.

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic

variable {u v : ℕ → ℝ}
variable {a : ℝ}

def IsExtraction (φ : ℕ → ℕ):=
  StrictMono φ

def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

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

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by sorry

Read more…

Challenge 20: If aₙ → L and M is an upper bound of aₙ, then L ≤ M

Lean 4 Challenges/Analysis/Limits

Prove that if the sequence \(a_{n}\) converges to \(L\) and \(M\) is an upper bound of \(a_{n}\) (that is, \(a_{n} ≤ M\) for all \(n\)), 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| < ε

def IsUB (a : ℕ → ℝ) (M : ℝ) : Prop :=
  ∀ n, a n ≤ M

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

example
  (ha : SeqLim a L)
  (hM : IsUB a M)
  : L ≤ M :=
by sorry

Read more…

Challenge 19: Convergent sequences are Cauchy sequences

Lean 4 Challenges/Analysis/Limits

Prove that convergent sequences are Cauchy sequences

To do so, complete the following Lean 4 theory:

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

variable {u : ℕ → ℝ}

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

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

def IsCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

example
  (h : SeqConv u)
  : IsCauchy u :=
by sorry

Read more…

Challenge 18: Convergence of the product of convergent sequences

Lean 4 Challenges/Analysis/Limits

Prove that if the sequence \(aₙ\) converges to \(L\) and \(bₙ\) converges to \(M\), then \(aₙbₙ\) converges to \(LM\).

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 c : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hc : ∀ n, c n = a n * b n)
  : SeqLim c (L * M) :=
by sorry

Read more…

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…