Ir al contenido principal

Reto 23: La sucesión constante aₙ = L converge a L

También disponible en:

English

Demostrar que la sucesión constante \(a_{n} = L\) converge a \(L\).

Para ello, completar la siguiente teoría:

import Mathlib.Tactic

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

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que para cada \(\varepsilon \in ℝ\) tal que \(\varepsilon > 0\), existe un \(k \in ℕ\), tal que \[ ∀ n ≥ k, |a_n - L| < \varepsilon \] Tomamos \(k = 0\). Para todo \(n ≥ k\), como \(a_n = L\), se tiene \[ \begin{array}{ll} |a_n - L| &= |L - L| \\ &= |0| \\ &= 0 \\ &< \varepsilon \\ \end{array} \]

2. Demostraciones con Lean 4

import Mathlib.Tactic

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

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

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  grind

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

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  refine ⟨0, by grind⟩

-- 3ª demostración
-- ===============

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
fun _ _ => ⟨0, by grind⟩

-- 4ª demostración
-- ===============

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := by grind
   _ = 0          := by grind
   _ < ε          := by grind

-- 5ª demostración
-- ===============

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := by rw [h n]
   _ = 0          := by norm_num
   _ < ε          := hε

-- 6ª demostración
-- ===============

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := by rw [h]
   _ = |0|        := by rw [sub_self L]
   _ = 0          := abs_zero
   _ < ε          := hε

-- 7ª demostración
-- ===============

theorem SeqLim_const
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |a n - L| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |a n - L| < ε
  rintro n -
  -- n : ℕ
  -- ⊢ |a n - L| < ε
  calc |a n - L|
     = |L - L|    := congrArg (|· - L|) (h n)
   _ = |0|        := congrArg abs (sub_self L)
   _ = 0          := abs_zero
   _ < ε          := hε

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

-- #check (abs_zero : |(0 : ℝ)| = 0)
-- #check (sub_self L : L - L = 0)

Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.

3. Soluciones colaborativas

¿Has encontrado una demostración distinta de las publicadas? Puedes compartirla en los comentarios de abajo siguiendo estos pasos:

  • Escribe tu demostración en live.lean-lang.org y comprueba que se compila sin errores.
  • Copia el código y publícalo en los comentarios de esta entrada, dentro de un bloque de código de Lean:
```lean
   -- tu demostración
```

Comentarios