Challenge 1: The sequence 1/n converges to 0
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
1. Proof in natural language
Let \(ε ∈ ℝ\) such that \(ε > 0\). By the Archimedean property, there exists \(k ∈ ℕ\) such that \[ 1 / ε < k \tag{1} \] We will show that, for all \(n ≥ k\), \(|a(n) - 0| < ε\). Indeed, let \[ n ≥ k \tag{2} \] Then, \begin{align} |a(n) - 0| &= |1/n - 0| \newline &= 1/n \newline &≤ 1/k &\text{[by (2)]} \newline &< ε &\text{[by (1)]} \newline \end{align}
2. Proofs in Lean 4
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε -- Solution 1 -- ========== namespace Solution1 lemma L1 {ε : ℝ} (hε : ε > 0) {k : ℕ} (hk : 1 / ε < k) : 0 < (k : ℝ) := (one_div_pos.mpr hε).trans hk lemma L2 {ε : ℝ} (hε : ε > 0) {k : ℕ} (hk : 1 / ε < k) : 1 / (k : ℝ) < ε := by apply (one_div_lt _ _).mp · -- ⊢ 1 / ε < ↑k gcongr · -- ⊢ 0 < ε gcongr · -- ⊢ 0 < ↑k exact L1 hε hk example (ha : ∀ n, a n = 1 / n) : SeqLim a 0 := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |a n - 0| < ε obtain ⟨k, hk⟩ := exists_nat_gt (1 / ε) -- k : ℕ -- hk : 1 / ε < ↑k use k --⊢ ∀ n ≥ k, |a n - 0| < ε intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n - 0| < ε calc |a n - 0| = |a n| := by grind _ = |1 / (n : ℝ)| := by grind _ = 1 / n := by grind _ ≤ 1 / k := by gcongr ; exact L1 hε hk _ < ε := L2 hε hk end Solution1 -- Solution 2 -- ========== namespace Solution2 lemma L1 {n : ℕ} : 0 ≤ 1 / (n : ℝ) := by -- ⊢ 0 ≤ 1 / ↑n apply div_nonneg · -- ⊢ 0 ≤ 1 exact zero_le_one · -- ⊢ 0 ≤ ↑n exact Nat.cast_nonneg n lemma L2 {n : ℕ} : |1 / (n : ℝ)| = 1 / n := by apply abs_of_nonneg -- ⊢ 0 ≤ 1 / ↑n exact L1 lemma L3 {ε : ℝ} (hε : ε > 0) {k : ℕ} (hk : 1 / ε < k) : 0 < (k : ℝ) := by calc (0 : ℝ) < 1 / ε := one_div_pos.mpr hε _ < k := hk lemma L4 {ε : ℝ} (hε : ε > 0) {k n : ℕ} (hk : 1 / ε < k) (hn : n ≥ k) : 1 / (n : ℝ) ≤ 1 / (k : ℝ) := by apply one_div_le_one_div_of_le · -- ⊢ 0 < ↑k exact L3 hε hk · -- ⊢ ↑k ≤ ↑n exact Nat.cast_le.mpr hn lemma L5 {ε : ℝ} (hε : ε > 0) {k : ℕ} (hk : 1 / ε < k) : 1 / (k : ℝ) < ε := by apply (one_div_lt _ _).mp · -- ⊢ 1 / ε < ↑k exact RCLike.ofReal_lt_ofReal.mp hk · -- ⊢ 0 < ε exact RCLike.ofReal_pos.mp hε · -- ⊢ 0 < ↑k exact L3 hε hk example (ha : ∀ n, a n = 1 / n) : SeqLim a 0 := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |a n - 0| < ε have h1 : ∃ (k : ℕ), 1 / ε < k := exists_nat_gt (1 / ε) obtain ⟨k, hk⟩ := h1 -- k : ℕ -- hk : 1 / ε < ↑k use k -- ⊢ ∀ n ≥ k, |a n - 0| < ε intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n - 0| < ε calc |a n - 0| = |a n| := by simp [sub_zero] _ = |1 / (n : ℝ)| := by rw [ha] _ = 1 / n := L2 _ ≤ 1 / k := L4 hε hk hn _ < ε := L5 hε hk end Solution2
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.
3. Collaborative solutions
Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:
- 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 ```
Comments