La sucesión aₙ = 1/n converge a 0
En Lean, una sucesión \(a₀, a₁, a₂, ...\) se puede representar mediante una función \((a : ℕ → ℝ)\) de forma que \(a(n)\) es \(aₙ\).
Se define que \(L\) es el límite de la sucesión \(a\), por
def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε
Demostrar que si para todo \(n\), \(aₙ = \frac{1}{n}\), entonces la sucesión \(a\) converge a \(0\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : ∀ n, a n = 1 / n) : LimSuc a 0 := by sorry
1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Por la propiedad arquimediana, existe \(N ∈ ℕ\) tal que \[\frac{1}{ε} < N \tag{1} \] Veamos que, para todo \(n ≥ N\), \(|a(n) - 0| < ε\). En efecto, sea \[n ≥ N \tag{2} \] Entonces, \begin{align} |a(n) - 0| &= |1/n - 0| \newline &= 1/n \newline &≤ 1/N &&\text{[por (2)]} \newline &< ε &&\text{[por (1)]} \newline \end{align}
2. Demostraciones con Lean4
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε -- 1ª demostración -- =============== lemma L1 {n : ℕ} : |1 / (n : ℝ)| = 1 / n := by apply abs_of_nonneg -- ⊢ 0 ≤ 1 / ↑n positivity variable {ε : ℝ} variable {N : ℕ} lemma L2 (hε : ε > 0) (hN : 1 / ε < N) : 0 < (N : ℝ) := by calc (0 : ℝ) < 1 / ε := by positivity _ < N := hN lemma L3 (hε : ε > 0) {n : ℕ} (hN : 1 / ε < N) (hn : n ≥ N) : 1 / (n : ℝ) ≤ 1 / (N : ℝ) := by apply one_div_le_one_div_of_le · -- ⊢ 0 < ↑N exact L2 hε hN · -- ⊢ ↑N ≤ ↑n gcongr lemma L4 (hε : ε > 0) (hN : 1 / ε < N) : 1 / (N : ℝ) < ε := by apply (one_div_lt _ _).mp · -- ⊢ 1 / ε < ↑N gcongr · -- ⊢ 0 < ε gcongr · -- ⊢ 0 < ↑N exact L2 hε hN example (ha : ∀ n, a n = 1 / n) : LimSuc a 0 := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ n ≥ N, |a n - 0| < ε have h1 : ∃ (N : ℕ), 1 / ε < N := exists_nat_gt (1 / ε) choose N hN using h1 -- N : ℕ -- hN : 1 / ε < ↑N use N --⊢ ∀ n ≥ N, |a n - 0| < ε intro n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |a n - 0| < ε calc |a n - 0| = |a n| := by norm_num _ = |1 / (n : ℝ)| := by rw [ha] _ = 1 / n := L1 _ ≤ 1 / N := L3 hε hN hn _ < ε := L4 hε hN -- 2ª demostración -- =============== lemma L0 {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 L1' {n : ℕ} : |1 / (n : ℝ)| = 1 / n := by apply abs_of_nonneg -- ⊢ 0 ≤ 1 / ↑n exact L0 lemma L2' (hε : ε > 0) (hN : 1 / ε < N) : 0 < (N : ℝ) := by calc (0 : ℝ) < 1 / ε := one_div_pos.mpr hε _ < N := hN lemma L3' (hε : ε > 0) {n : ℕ} (hN : 1 / ε < N) (hn : n ≥ N) : 1 / (n : ℝ) ≤ 1 / (N : ℝ) := by apply one_div_le_one_div_of_le · -- ⊢ 0 < ↑N exact L2' hε hN · -- ⊢ ↑N ≤ ↑n exact Nat.cast_le.mpr hn lemma L4' (hε : ε > 0) (hN : 1 / ε < N) : 1 / (N : ℝ) < ε := by apply (one_div_lt _ _).mp · -- ⊢ 1 / ε < ↑N exact RCLike.ofReal_lt_ofReal.mp hN · -- ⊢ 0 < ε exact RCLike.ofReal_pos.mp hε · -- ⊢ 0 < ↑N exact L2' hε hN example (ha : ∀ n, a n = 1 / n) : LimSuc a 0 := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ n ≥ N, |a n - 0| < ε have h1 : ∃ (N : ℕ), 1 / ε < N := exists_nat_gt (1 / ε) choose N hN using h1 -- N : ℕ -- hN : 1 / ε < ↑N use N -- ⊢ ∀ n ≥ N, |a n - 0| < ε intro n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |a n - 0| < ε calc |a n - 0| = |a n| := by simp [sub_zero] _ = |1 / (n : ℝ)| := by rw [ha] _ = 1 / n := L1' _ ≤ 1 / N := L3' hε hN hn _ < ε := L4' hε hN -- Lemas usados -- ============ variable (x y : ℝ) variable (m n : ℕ) #check (Nat.cast_le : ↑m ≤ ↑n ↔ m ≤ n) #check (Nat.cast_nonneg n : 0 ≤ n) #check (RCLike.ofReal_lt_ofReal : ↑x < ↑y ↔ x < y) #check (abs_of_nonneg : 0 ≤ x → |x| = x) #check (div_nonneg : 0 ≤ x -> 0 ≤ y -> 0 ≤ x / y) #check (exists_nat_gt x : ∃ n : ℕ, x < n) #check (one_div_le_one_div_of_le : 0 < x → x ≤ y → 1 / y ≤ 1 / x) #check (one_div_lt : 0 < x → 0 < y → (1 / x < y ↔ 1 / y < x)) #check (one_div_pos : 0 < 1 / x ↔ 0 < x) #check (zero_le_one : 0 ≤ 1)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.