Ir al contenido principal

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 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

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 SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

variable {a b : ℕ → ℝ}
variable {L : ℝ}

-- 1ª demostración
-- ===============

example
  (ha : SeqLim a L)
  (hb : ∀ n, b n = |a n|)
  : SeqLim 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 : SeqLim a L)
  (hb : ∀ n, b n = |a n|)
  : SeqLim 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 : SeqLim a L)
  (hb : ∀ n, b n = |a n|)
  : SeqLim 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 : SeqLim a L)
  (hb : ∀ n, b n = |a n|)
  : SeqLim 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 : SeqLim a L)
  (hb : ∀ n, b n = |a n|)
  : SeqLim 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.