Skip to main content

Posts about Sequences (old posts, page 1)

RSS feed (Sequences, en)

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 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…

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

Analysis/Limits

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

Read more…

If aₙ converges to L and bₙ to M, then aₙ+bₙ converges to L+M.

Analysis/Limits

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

To do so, complete the following Lean 4 theory:

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

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

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

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  : SeqLim (a + b) (L + M) :=
by
  sorry

Read more…

Challenge 3: If aₙ converges to L, then 2aₙ converges to 2L

Lean 4 Challenges/Analysis/Limits

Prove in Lean 4 that if the sequence \(aₙ\) converges to \(L\), then \(2aₙ\) converges to \(2L\).

To do so, complete the following Lean 4 theory:

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

variable {a : ℕ → ℝ}

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

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

Read more…

Challenge 2: The sequence 1, -1, 1, -1,... is not convergent

Lean 4 Challenges/Analysis/Limits

Prove that the sequence defined by 1, -1, 1, -1, ... does not converge.

To do so, the following proof in Lean 4 is to be completed:

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

variable {a : ℕ → ℝ}

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

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

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

Read more…