Reto 21: Las subsucesiones tienen el mismo límite que la sucesión
Una subsucesión se obtiene aplicando a la sucesión original una función de extracción; es decir, una función \(φ : ℕ \to ℕ\) estrictamente creciente. Por ejemplo, la subsucesión \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] se obtiene con la función de extracción \(\varphi\) definida por \(\varphi(n) = 2n\).
Las definiciones anteriores se formalizan en Lean 4 como:
-- φ es una función de extracción. def IsExtraction (φ : ℕ → ℕ) := StrictMono φ -- v es una subsucesión de u. def Subseq (v u : ℕ → ℝ) := ∃ φ, IsExtraction φ ∧ v = u ∘ φ -- a es el límite de u. def SeqLim (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε
Demostrar que toda subsucesión de una sucesión convergente converge al mismo límite que la sucesión.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic variable {u v : ℕ → ℝ} variable {a : ℝ} def IsExtraction (φ : ℕ → ℕ):= StrictMono φ def Subseq (v u : ℕ → ℝ) := ∃ φ, IsExtraction φ ∧ v = u ∘ φ def SeqLim (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε example (hv : Subseq v u) (ha : SeqLim u a) : SeqLim v a := by sorry
1. Demostración en lenguaje natural
Usaremos el siguiente lema: Si \(\varphi\) es una función de extracción, entonces \[ \forall n, n \leq \varphi(n) \]
Por ser \(v\) una subsucesión de \(u\), existe una función de extracción \(\varphi\) tal que \[ v = u ∘ \varphi \tag{1} \]
Tenemos que demostrar que para cada \(\varepsilon > 0\), existe un \(k \in \mathbb{N}\) tal que \[ \forall n \geq k, |v(n) - a| < \varepsilon \tag{2} \]
Puesto que \(a\) es el límite de \(u\), existe un \(k \in \mathbb{N}\) tal que \[ \forall n \geq k, |u(n) - a| < \varepsilon \tag{3} \]
Veamos que \(k\) verifica (2). Para ello, sea \(n \geq k\). Entonces, \[ \varphi(n) \geq k \tag{4} \] ya que \[ \begin{array}{llll} \varphi(n) &\geq n &&\text{[por el Lema]} \\ &\geq k \\ \end{array} \] Luego, \[ \begin{array}{llll} |v(n) - a| &= |(u ∘ \varphi)(n) - a| &&\text{[por (1)]} \\ &= |u(\varphi(n)) - a| \\ &< \varepsilon &&\text{[por (3) y (4)]} \end{array} \]
2. Demostraciones con Lean4
import Mathlib.Data.Real.Basic variable {u v : ℕ → ℝ} variable {a : ℝ} -- φ es una función de extracción. def IsExtraction (φ : ℕ → ℕ):= StrictMono φ -- v es una subsucesión de u. def Subseq (v u : ℕ → ℝ) := ∃ φ, IsExtraction φ ∧ v = u ∘ φ -- a es el límite de u. def SeqLim (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε -- 1ª demostración -- =============== example (hv : Subseq v u) (ha : SeqLim u a) : SeqLim v a := by obtain ⟨φ, hφ, hφ'⟩ := hv -- φ : ℕ → ℕ -- hφ : IsExtraction φ -- hφ' : v = u ∘ φ intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |v n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε use k -- ⊢ ∀ n ≥ k, |v n - a| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |v n - a| < ε have h1 : φ n ≥ k := calc φ n ≥ n := StrictMono.le_apply hφ _ ≥ k := hn calc |v n - a| = |(u ∘ φ ) n - a| := by rw [hφ'] _ = |u (φ n) - a| := rfl _ < ε := hk (φ n) h1 -- 2ª demostración -- =============== example (hv : Subseq v u) (ha : SeqLim u a) : SeqLim v a := by obtain ⟨φ, hφ, rfl⟩ := hv -- φ : ℕ → ℕ -- hφ : IsExtraction φ -- ⊢ SeqLim (u ∘ φ) a intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε use k -- ⊢ ∀ n ≥ k, |(u ∘ φ) n - a| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |(u ∘ φ) n - a| < ε have h1 : φ n ≥ k := calc φ n ≥ n := hφ.le_apply _ ≥ k := hn calc |(u ∘ φ) n - a| _ = |u (φ n) - a| := rfl _ < ε := hk (φ n) h1 -- 3ª demostración -- =============== example (hv : Subseq v u) (ha : SeqLim u a) : SeqLim v a := by obtain ⟨φ, hφ, rfl⟩ := hv -- φ : ℕ → ℕ -- hφ : IsExtraction φ -- ⊢ SeqLim (u ∘ φ) a intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε use k -- ⊢ ∀ n ≥ k, |(u ∘ φ) n - a| < ε intros n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |(u ∘ φ) n - a| < ε apply hk -- ⊢ φ n ≥ k apply le_trans hn -- ⊢ n ≤ φ n exact hφ.le_apply -- 4ª demostración -- =============== example (hv : Subseq v u) (ha : SeqLim u a) : SeqLim v a := by obtain ⟨φ, hφ, rfl⟩ := hv -- φ : ℕ → ℕ -- hφ : IsExtraction φ -- ⊢ SeqLim (u ∘ φ) a intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε obtain ⟨k, hk⟩ := ha ε hε -- k : ℕ -- hk : ∀ n ≥ k, |u n - a| < ε exact ⟨k, fun n hn ↦ hk (φ n) (le_trans hn hφ.le_apply)⟩
Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.