Skip to content

Latest commit

 

History

History
227 lines (196 loc) · 7.11 KB

Unicidad_del_limite_de_las_sucesiones_convergentes.md

File metadata and controls

227 lines (196 loc) · 7.11 KB
Título Autor
Unicidad del límite de las sucesiones convergentes
José A. Alonso

[mathjax]

En Lean, una sucesión \(u₀, u₁, u₂, ...\) se puede representar mediante una función \((u : ℕ → ℝ)\) de forma que \(u(n)\) es \(uₙ\).

Se define que \(a\) es el límite de la sucesión \(u\), por

   def limite : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

Demostrar con Lean4 que cada sucesión tiene como máximo un límite.

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

import Mathlib.Data.Real.Basic
variable {u : ℕ → ℝ}
variable {a b : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
  by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que si \(u\) es una sucesión y \(a\) y \(b\) son límites de \(u\), entonces \(a = b\). Para ello, basta demostrar que \(a ≤ b\) y \(b ≤ a\).

Demostraremos que \(b ≤ a\) por reducción al absurdo. Supongamos que \(b ≰ a\). Sea \(ε = b - a\). Entonces, ε/2 > 0 y, puesto que \(a\) es un límite de \(u\), existe un \(A ∈ ℕ\) tal que \[ (∀n ∈ ℕ)\left[n ≥ A → |u(n) - a| < \frac{ε}{2}\right] \tag{1} \] y, puesto que \(b\) también es un límite de \(u\), existe un \(B ∈ ℕ\) tal que \[ (∀n ∈ ℕ)\left[n ≥ B → |u(n) - b| < \frac{ε}{2}\right] \tag{2} \] Sea \(N = máx(A, B)\). Entonces, \(N ≥ A\) y \(N ≥ B\) y, por (2) y (3), se tiene \begin{align} |u(N) - a| &< \frac{ε}{2} \tag{3} \\ |u(N) - b| &< \frac{ε}{2} \tag{4} \end{align} Para obtener una contradicción basta probar que \(ε < ε\). Su prueba es \begin{align} ε &= b - a \\ &= |b - a| \\ &= |(b - a) + (u(N) - u(N))| \\ &= |(u(N) - a) + (b - u(N))| \\ &≤ |u(N) - a| + |b - u(N)| \\ &= |u(N) - a| + |u(N) - b| \\ &< \frac{ε}{2} + \frac{ε}{2} && \text{[por (3) y (4)]} \\ &= ε \end{align}

La demostración de \(a ≤ b\) es análoga a la anterior.

2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable {u : ℕ → ℝ}
variable {a b : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración del lema auxiliar
-- =================================

example
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
by
  by_contra h
  -- h : ¬b ≤ a
  -- ⊢ False
  let ε := b - a
  have hε : ε > 0 := sub_pos.mpr (not_le.mp h)
  have hε2 : ε / 2 > 0 := half_pos hε
  cases' ha (ε/2) hε2 with A hA
  -- A : ℕ
  -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2
  cases' hb (ε/2) hε2 with B hB
  -- B : ℕ
  -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2
  let N := max A B
  have hAN : A ≤ N := le_max_left A B
  have hBN : B ≤ N := le_max_right A B
  specialize hA N hAN
  -- hA : |u N - a| < ε / 2
  specialize hB N hBN
  -- hB : |u N - b| < ε / 2
  have h2 : ε < ε := by calc
    ε = b - a                   := rfl
    _ = |b - a|                 := (abs_of_pos hε).symm
    _ = |(b - a) + 0|           := by {congr ; exact (add_zero (b - a)).symm}
    _ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm}
    _ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring)
    _ ≤ |u N - a| + |b - u N|   := abs_add (u N - a) (b - u N)
    _ = |u N - a| + |u N - b|   := congrArg (|u N - a| + .) (abs_sub_comm b (u N))
    _ < ε / 2 + ε / 2           := add_lt_add hA hB
    _ = ε                       := add_halves ε
  have h3 : ¬(ε < ε) := lt_irrefl ε
  show False
  exact h3 h2

-- 2ª demostración del lema auxiliar
-- =================================

lemma aux
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
by
  by_contra h
  -- h : ¬b ≤ a
  -- ⊢ False
  let ε := b - a
  cases' ha (ε/2) (by linarith) with A hA
  -- A : ℕ
  -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2
  cases' hb (ε/2) (by linarith) with B hB
  -- B : ℕ
  -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2
  let N := max A B
  have hAN : A ≤ N := le_max_left A B
  have hBN : B ≤ N := le_max_right A B
  specialize hA N hAN
  -- hA : |u N - a| < ε / 2
  specialize hB N hBN
  -- hB : |u N - b| < ε / 2
  rw [abs_lt] at hA hB
  -- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2
  -- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2
  linarith

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

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (aux hb ha) (aux ha hb)

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

-- variable (c d : ℝ)
-- #check (not_le : ¬a ≤ b ↔ b < a)
-- #check (sub_pos : 0 < a - b ↔ b < a)
-- #check (half_pos : a > 0 → a / 2 > 0)
-- #check (le_max_left a b : a ≤ max a b)
-- #check (le_max_right a b : b ≤ max a b)
-- #check (abs_lt : |a| < b ↔ -b < a ∧ a < b)
-- #check (abs_of_pos : 0 < a → |a| = a)
-- #check (add_zero a : a + 0 = a)
-- #check (sub_self a : a - a = 0)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (abs_sub_comm a b : |a - b| = |b - a|)
-- #check (add_lt_add : a < b → c < d → a + c < b + d)
-- #check (add_halves a : a / 2 + a / 2 = a)
-- #check (lt_irrefl a : ¬a < a)
-- #check (le_antisymm : a ≤ b → b ≤ a → a = b)

Demostraciones interactivas

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

3. Demostraciones con Isabelle/HOL

theory Unicidad_del_limite_de_las_sucesiones_convergentes
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

lemma aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed

theorem
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1) by (rule aux)
next
  show "b ≤ a" using assms(1) assms(2) by (rule aux)
qed

end