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
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
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
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
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
Prove that there are infinitely many prime numbers.
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry
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
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
In Lean, a sequence \(a₀, a₁, a₂,...\) can be represented by a function \(a : ℕ → ℝ\) so that \(a(n)\) is \(aₙ\).
The statement that \(L\) is the limit of the sequence \(a\) is defined by
def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε
Prove that if \(aₙ = 1/n\) for all \(n\), then the sequence \(a\) converges to 0.
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, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε example (ha : ∀ n, a n = 1 / n) : SeqLim a 0 := by sorry
I have started publishing the series Mathematical challenges in Lean 4.
The format is simple: each week I will post a mathematical problem so that anyone interested can share their solutions in Lean 4.
At the end of the week I will publish the solutions to the challenge, which will follow this scheme:
grind.norm_num, ring, positivity or linarith.Through this process of successive refinement, the aim is for the final proof to correspond, as far as possible, to the one written in natural language.