Reto 18: Convergencia del producto de sucesiones convergentes
El reto de esta semana consiste en demostrar en Lean 4 que si la sucesión \(aₙ\) converge a \(L\) y \(bₙ\) converge a \(M\), entonces \(aₙbₙ\) converge a \(LM\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b c : ℕ → ℝ} variable {L M : ℝ} example (ha : LimSuc a L) (hb : LimSuc b M) (hc : ∀ n, c n = a n * b n) : LimSuc c (L * M) := by sorry
1. Demostración en lenguaje natural
Sea \(ε > 0\). Como \(a_n\) converge a \(L\), existe \(N_1\) tal que si \(n ≥ N_1\), entonces \[ |a_n − L| < 1 \] Por tanto, para \(n ≥ N_1\) se tiene que \[ \begin{array}{ll} |a_n| &= |a_n − L + L| \\ &≤ |a_n − L| + |L| \\ &< 1 + |L| \\ \end{array} \] Definamos \[ C = 1 + |L| \] Entonces \[ C > 0 \] y, para \(n ≥ N_1\) \[ |a_n| ≤ C \] Ahora, como \(a_n\) converge a \(L\), existe \(N_2\) tal que si \(n ≥ N_2\), entonces \[ |a_n − L| < \dfrac{ε}{2(|M| + 1)} \] Por otra parte, como \(b_n\) converge a \(M\), existe \(N_3\) tal que si \(n ≥ N_3\), entonces \[ |b_n − M| < \dfrac{ε}{2C} \] Sea \[ N = \max\{N_1,N_2,N_3\} \] Si \(n ≥ N\), entonces se cumplen las tres desigualdades anteriores. Ahora estimamos: \[ |a_nb_n − LM| \] Sumamos y restamos \(a_nM\): \[ a_nb_n − LM = a_nb_n − a_nM + a_nM − LM \] Entonces \[ |a_nb_n − LM| = |a_n(b_n − M) + M(a_n − L)| \] Por la desigualdad triangular, \[ |a_nb_n − LM| ≤ |a_n||b_n − M| +|M||a_n − L| \] Como \(n ≥ N_1\),tenemos \[ |a_n| ≤ C \] Luego, \[ |a_nb_n − LM| ≤ C|b_n − M| + |M||a_n − L| \] Usando las cotas elegidas, \[ \begin{array}{ll} C|b_n − M| &< C \dfrac{ε}{2C} \\ &= \dfrac{ε}{2} \end{array} \] y \[ |M||a_n − L| < |M| \dfrac{ε}{2(|M| + 1)} \] Como \[ \dfrac{|M|}{|M| + 1} < 1 \] se sigue que \[ |M| \dfrac{ε}{2(|M| + 1)} < \dfrac{ε}{2} \] Por tanto, \[ \begin{array}{ll} |a_nb_n − LM| &< \dfrac{ε}{2} + \dfrac{ε}{2} \\ &= ε \end{array} \] Así, para todo \(ε > 0\) existe \(N\) tal que si \(n ≥ N\), entonces \[ |a_nb_n − LM| < ε \] Esto prueba que, para todo \(ε > 0\), existe \(N\) tal que \(|a_nb_n − LM| < ε\) siempre que \(n ≥ N\), es decir, \(a_nb_n\) converge a \(LM\).
2. Demostraciones en Lean 4
import Mathlib.Data.Real.Basic import Mathlib.Tactic def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b c : ℕ → ℝ} variable {L M : ℝ} -- 1ª solución -- =========== example (ha : LimSuc a L) (hb : LimSuc b M) (hc : ∀ n, c n = a n * b n) : LimSuc c (L * M) := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |c n - L * M| < ε obtain ⟨N₁, hN₁⟩ := ha 1 (by positivity) -- N₁ : ℕ -- hN₁ : ∀ n ≥ N₁, |a n - L| < 1 have h1 : ∀ n ≥ N₁, |a n| < 1 + |L| := by grind set C := 1 + |L| -- h1 : ∀ n ≥ N₁, |a n| < C have h2 : C > 0 := by grind obtain ⟨N₂, hN₂⟩ := ha (ε / (2 * (|M| + 1))) (by positivity) -- N₂ : ℕ -- hN₂ : ∀ n ≥ N₂, |a n - L| < ε / (2 * (|M| + 1)) obtain ⟨N₃, hN₃⟩ := hb (ε / (2 * C)) (by positivity) -- N₃ : ℕ -- hN₃ : ∀ n ≥ N₃, |b n - M| < ε / (2 * C) set N := max N₁ (max N₂ N₃) use N -- ⊢ ∀ n ≥ N, |c n - L * M| < ε intro n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |c n - L * M| < ε have h3 : n ≥ N₁ := by grind have h4 : n ≥ N₂ := by grind have h5 : n ≥ N₃ := by grind have h6 : |a n| < C := by grind have h7 : |b n - M| < ε / (2 * C) := by grind have h8 : |a n - L| < ε / (2 * (|M| + 1)) := by grind have h9 : |M| * (ε / (2 * (|M| + 1))) < ε / 2 := by field_simp -- ⊢ |M| < |M| + 1 norm_num calc |c n - L * M| = |a n * b n - L * M| := by grind _ = |a n * (b n - M) + M * (a n - L)| := by grind _ ≤ |a n * (b n - M)| + |M * (a n - L)| := by grind _ = |a n| * |b n - M| + |M| * |a n - L| := by grind _ ≤ C * |b n - M| + |M| * |a n - L| := by gcongr _ < C * (ε / (2 * C)) + |M| * |a n - L| := by gcongr _ ≤ C * (ε / (2 * C)) + |M| * (ε / (2 * (|M| + 1))) := by gcongr _ = ε / 2 + |M| * (ε / (2 * (|M| + 1))) := by grind _ < ε / 2 + ε / 2 := by grind _ = ε := by grind -- 2ª solución -- =========== lemma L1 (h : LimSuc a L) : ∃ k, ∀ n ≥ k, |a n| < 1 + |L| := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n| < |L| + 1 calc |a n| = |(a n - L) + L| := congrArg abs (sub_add_cancel (a n) L).symm _ ≤ |a n - L| + |L| := abs_add_le (a n - L) L _ < 1 + |L| := (add_lt_add_iff_right |L|).mpr (hk n hn) example (ha : LimSuc a L) (hb : LimSuc b M) (hc : ∀ n, c n = a n * b n) : LimSuc c (L * M) := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |c n - L * M| < ε obtain ⟨N₁, hN₁⟩ := L1 ha -- N₁ : ℕ -- hN₁ : ∀ n ≥ N₁, |a n| < 1 + |L| set C := 1 + |L| with hC -- hC : C = 1 + |L| have h2 : C > 0 := by positivity obtain ⟨N₂, hN₂⟩ := ha (ε / (2 * (|M| + 1))) (by positivity) -- N₂ : ℕ -- hN₂ : ∀ n ≥ N₂, |a n - M| < ε / (2 * (|M| + 1)) obtain ⟨N₃, hN₃⟩ := hb (ε / (2 * C)) (by positivity) -- N₃ : ℕ -- hN₃ : ∀ n ≥ N₃, |b n - M| < ε / (2 * C) set N := max N₁ (max N₂ N₃) use N -- ⊢ ∀ n ≥ N, |c n - L * M| < ε intro n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |c n - L * M| < ε have h3 : n ≥ N₁ := by omega have h4 : n ≥ N₂ := by omega have h5 : n ≥ N₃ := by omega have h6 : |a n| < C := by calc |a n| < 1 + |L| := hN₁ n h3 _ = C := rfl have h7 : |b n - M| < ε / (2 * C) := hN₃ n h5 have h8 : |a n - L| < ε / (2 * (|M| + 1)) := hN₂ n h4 have h9 : |M| * (ε / (2 * (|M| + 1))) < ε / 2 := by field_simp -- ⊢ |M| < |M| + 1 norm_num calc |c n - L * M| = |a n * b n - L * M| := congrArg (|· - L * M|) (hc n) _ = |a n * (b n - M) + M * (a n - L)| := by ring_nf _ ≤ |a n * (b n - M)| + |M * (a n - L)| := abs_add_le (a n * (b n - M)) (M * (a n - L)) _ = |a n| * |b n - M| + |M| * |a n - L| := by simp only [abs_mul] _ ≤ C * |b n - M| + |M| * |a n - L| := by gcongr _ < C * (ε / (2 * C)) + |M| * |a n - L| := by gcongr _ ≤ C * (ε / (2 * C)) + |M| * (ε / (2 * (|M| + 1))) := by gcongr _ = ε / 2 + |M| * (ε / (2 * (|M| + 1))) := by field_simp _ < ε / 2 + ε / 2 := by gcongr _ = ε := add_halves ε
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.