Las sucesiones convergentes están acotadas

José A. Alonso

28-05-2024

Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir, \[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by sorry

1. Demostración en lenguaje natural

Puesto que la sucesión \(u_n\) es convergente, existe un \(a ∈ ℝ\) tal que \[ \lim(u_n) = a \] Luego, existe un \(k ∈ ℕ\) tal que \[ (∀ n ∈ ℕ)[n ≥ k → |u_n - a | < 1] \tag{1} \] Veamos que \[ (∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ 1 + |a]] \] Para ello, sea \(n ∈ ℕ\) tal que \[ n ≥ k \tag{2} \] Entonces, \begin{align} |u_n| &= |u_n - a + a| \newline &≤ |u_n - a| + |a| \newline &≤ 1 + |a| &&\text{[por (1) y (2)]} \end{align}

2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

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

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by
  cases' h with a ua
  -- a : ℝ
  -- ua : limite u a
  cases' ua 1 zero_lt_one with k h
  -- k : ℕ
  -- h : ∀ (n : ℕ), n ≥ k → |u n - a| ≤ 1
  use k, 1 + |a|
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n| ≤ 1 + |a|
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n| ≤ 1 + |a|
  specialize h n hn
  -- ⊢ |u n| ≤ 1 + |a|
  calc |u n|
       = |u n - a + a|   := congr_arg abs (eq_add_of_sub_eq rfl)
     _ ≤ |u n - a| + |a| := abs_add (u n - a) a
     _ ≤ 1 + |a|         := add_le_add_right h |a|

-- 2ª demostración
-- ===============

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by
  cases' h with a ua
  -- a : ℝ
  -- ua : limite u a
  cases' ua 1 zero_lt_one with k h
  -- k : ℕ
  -- h : ∀ (n : ℕ), n ≥ k → |u n - a| ≤ 1
  use k, 1 + |a|
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n| ≤ 1 + |a|
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n| ≤ 1 + |a|
  specialize h n hn
  -- h : |u n - a| ≤ 1
  calc |u n|
       = |u n - a + a|   := by ring_nf
     _ ≤ |u n - a| + |a| := abs_add (u n - a) a
     _ ≤ 1 + |a|         := by linarith

-- Lemas usados
-- ============

-- variable (a b c : ℝ)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (add_le_add_right : b ≤ c → ∀ a,  b + a ≤ c + a)
-- #check (eq_add_of_sub_eq :  a - c = b → a = b + c)
-- #check (zero_lt_one : 0 < 1)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory Acotacion_de_convergentes
imports Main HOL.Real
begin

(* (limite u c) expresa que el límite de u es c. *)
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (convergente u) expresa que u es convergente. *)
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"

(* 1ª demostración *)

lemma
  assumes "convergente u"
  shows   "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
proof -
  obtain a where "limite u a"
    using assms convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"
    using limite_def zero_less_one by blast
  have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"
  proof (intro allI impI)
    fix n
    assume hn : "n ≥ k"
    have "¦u n¦ = ¦u n - a + a¦"     by simp
    also have "… ≤ ¦u n - a¦ + ¦a¦" by simp
    also have "… ≤ 1 + ¦a¦"         by (simp add: hk hn)
    finally show "¦u n¦ ≤ 1 + ¦a¦"  .
  qed
  then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
    by (intro exI)
qed

end