Prove that for every \(n \in ℕ\), \(n(n+1)(2n+1)\) is divisible by \(6\).
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic variable (n : ℕ) example : 6 ∣ n * (n + 1) * (2 * n + 1) := by sorry
Prove that there exists \(k ∈ ℕ\) such that, for all \(n \in ℕ\), \((n + k)^{2} ≤ 2^{n+k}\).
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := by sorry
Prove that, for all \(n \in ℕ\), \(2n + 9 ≤ 2^{n+4}\).
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic variable (n : ℕ) example : 2 * n + 9 ≤ 2 ^ (n + 4) := by sorry
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
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
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
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
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
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
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