Reto 11: Si aₙ converge a L, entonces |aₙ| converge a |L|
El reto de esta semana consiste en demostrar en Lean 4 que si la sucesión \(a_n\) converge a \(L\), entonces \(|a_n|\) converge a \(|L|\).
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 : ℕ → ℝ} variable {L : ℝ} example (ha : LimSuc a L) (hb : ∀ n, b n = |a n|) : LimSuc b |L| := by sorry
1. Demostración en lenguaje natural
Sea \(b_n = |a_n|\), para todo n. Tenemos que demostrar que \(b_n\) converge a \(|L|\). Para ello, sea \(ε > 0\) y hay que probar que existe un \(k\) tal que, \[ ∀ n ≥ k, |b_n - |L|| < ε \tag{1} \]
Puesto que \(a_n\) converge a \(L\), existe un \(k\) tal que, \[ ∀ n ≥ k, |a_n - L| < ε \tag{2} \] Veamos que para dicho \(k\) se cumple (1). En efecto, sea \[ n ≥ k. \tag{3} \] Entonces, \[ \begin{array}{llll} |b_n - |L|| &= ||a_n| - |L|| \\ &≤ |a_n - L| &&\text{[por la desigualdad triangular inversa]} \\ &< ε &&\text{[por (2) y (3)]} \\ \end{array} \]
2. Demostraciones con Lean4
import Mathlib.Data.Real.Basic import Mathlib.Tactic def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε variable {a b : ℕ → ℝ} variable {L : ℝ} -- 1ª demostración -- =============== example (ha : LimSuc a L) (hb : ∀ n, b n = |a n|) : LimSuc b |L| := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |b n - |L|| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < ε use k -- ⊢ ∀ n ≥ k, |b n - |L|| < ε intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |b n - |L|| < ε grind -- 2ª demostración -- =============== example (ha : LimSuc a L) (hb : ∀ n, b n = |a n|) : LimSuc b |L| := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |b n - |L|| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < ε refine ⟨k, fun _ _ => by grind⟩ -- 3ª demostración -- =============== example (ha : LimSuc a L) (hb : ∀ n, b n = |a n|) : LimSuc b |L| := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |b n - |L|| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < ε use k -- ⊢ ∀ n ≥ k, |b n - |L|| < ε intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |b n - |L|| < ε calc |b n - (|L|)| = |(|a n|) - (|L|)| := by grind _ ≤ |a n - L| := by grind _ < ε := by grind -- 4ª demostración -- =============== example (ha : LimSuc a L) (hb : ∀ n, b n = |a n|) : LimSuc b |L| := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |b n - |L|| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < ε use k -- ⊢ ∀ n ≥ k, |b n - |L|| < ε intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |b n - |L|| < ε calc |b n - (|L|)| = |(|a n|) - (|L|)| := by rw [hb n] _ ≤ |a n - L| := abs_abs_sub_abs_le (a n) L _ < ε := hk n hn -- 5ª demostración -- =============== example (ha : LimSuc a L) (hb : ∀ n, b n = |a n|) : LimSuc b |L| := by intro ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |b n - |L|| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < ε use k -- ⊢ ∀ n ≥ k, |b n - |L|| < ε intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |b n - |L|| < ε calc |b n - (|L|)| = |(|a n|) - (|L|)| := congrArg (|· - (|L|)|) (hb n) _ ≤ |a n - L| := abs_abs_sub_abs_le (a n) L _ < ε := hk n hn -- Lemas usados -- ============ variable (x y : ℝ) #check (abs_abs_sub_abs_le x y : |(|x|) - (|y|)| ≤ |x - y|)
En el siguiente vídeo se explica paso a paso la construcción de las soluciones:
Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.