Límite de sucesiones – Página 2

Unicidad del límite de las sucesiones convergentes

PorJosé A. Alonso 6 febrero 202419 febrero 2024

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

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

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)

100

101

102

103

104

105

106

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

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)

show "b ≤ a" using assms(1) assms(2) by (rule aux)

qed

end

Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b

PorJosé A. Alonso 5 febrero 20246 mayo 2024

Demostrar con Lean4 que si la sucesión \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).

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

import Mathlib.Data.Real.Basic
variable {s t : ℕ → ℝ} {a b c : ℝ}

def limite (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
by sorry

import Mathlib.Data.Real.Basic

variable {s t : ℕ → ℝ} {a b c : ℝ}

def limite (s : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

by sorry

La sucesión constante sₙ = c converge a c

PorJosé A. Alonso 2 febrero 202418 febrero 2024

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

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

def limite (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

1 2	def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, \|s n - a\| < ε

Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).

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

import Mathlib.Data.Real.Basic

def limite (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

example : limite (fun _ : ℕ ↦ c) c :=
by sorry

import Mathlib.Data.Real.Basic

def limite (s : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

example : limite (fun _ : ℕ ↦ c) c :=

by sorry

Los límites son menores o iguales que las cotas superiores

PorJosé A. Alonso 16 septiembre 202111 septiembre 2021

En Lean, se puede definir que a es el límite de la sucesión u por

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

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, \|u n - a\| < ε

y que a es una cota superior de u por

   def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
     ∀ n, u n ≤ a

1 2	def cota_superior (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a

Demostrar que si x es el límite de la sucesión u e y es una cota superior de u, entonces x ≤ y.

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

import data.real.basic

variable  (u : ℕ → ℝ)
variables (x y : ℝ)

notation `|`x`|` := abs x

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

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
  ∀ n, u n ≤ a

example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variables (x y : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=

∀ n, u n ≤ a

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable  (u : ℕ → ℝ)
variables (x y : ℝ)

notation `|`x`|` := abs x

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

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
  ∀ n, u n ≤ a

lemma aux :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split ; linarith,
end

-- 1º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k rfl.ge,
  replace hk : -ε < u k - x := neg_lt_of_abs_lt hk,
  replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk,
  apply le_of_lt,
  exact lt_add_of_lt_add_right hk (hy k),
end

-- 2º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k rfl.ge,
  apply le_of_lt,
  calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk)
     ... ≤ y + ε   : add_le_add_right (hy k) ε,
end

-- 3º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k (by linarith),
  rw abs_lt at hk,
  linarith [hy k],
end

import data.real.basic

variable (u : ℕ → ℝ)

variables (x y : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=

∀ n, u n ≤ a

lemma aux :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split ; linarith,

end

-- 1º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k rfl.ge,

replace hk : -ε < u k - x := neg_lt_of_abs_lt hk,

replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk,

apply le_of_lt,

exact lt_add_of_lt_add_right hk (hy k),

end

-- 2º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k rfl.ge,

apply le_of_lt,

calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk)

... ≤ y + ε : add_le_add_right (hy k) ε,

end

-- 3º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k (by linarith),

rw abs_lt at hk,

linarith [hy k],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Los_limites_son_menores_o_iguales_que_las_cotas_superiores
imports Main HOL.Real
begin

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

definition cota_superior :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "cota_superior u c ⟷ (∀n. u n ≤ c)"

(* 1ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then have "¦u k - x¦ < ε"
    by simp
  then have "-ε < u k - x"
    by simp
  then have "x < u k + ε"
    by simp
  moreover have "u k ≤ y"
    using assms(2) cota_superior_def by simp
  ultimately show "x ≤ y + ε"
    by simp
qed

(* 2ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then have "x < u k + ε"
    by auto
  moreover have "u k ≤ y"
    using assms(2) cota_superior_def by simp
  ultimately show "x ≤ y + ε"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then show "x ≤ y + ε"
    using assms(2) cota_superior_def
    by (smt (verit) order_refl)
qed

end

theory Los_limites_son_menores_o_iguales_que_las_cotas_superiores

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition cota_superior :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"cota_superior u c ⟷ (∀n. u n ≤ c)"

(* 1ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then have "¦u k - x¦ < ε"

by simp

then have "-ε < u k - x"

by simp

then have "x < u k + ε"

by simp

moreover have "u k ≤ y"

using assms(2) cota_superior_def by simp

ultimately show "x ≤ y + ε"

by simp

qed

(* 2ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then have "x < u k + ε"

by auto

moreover have "u k ≤ y"

using assms(2) cota_superior_def by simp

ultimately show "x ≤ y + ε"

by simp

qed

(* 3ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then show "x ≤ y + ε"

using assms(2) cota_superior_def

by (smt (verit) order_refl)

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Límite de sucesiones no decrecientes

PorJosé A. Alonso 6 septiembre 20213 septiembre 2021

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

En Lean, se define que a es el límite de la sucesión u, por

   def limite (u: ℕ → ℝ) (a: ℝ) :=
     ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε
<pre lang="text">
donde se usa la notación |x| para el valor absoluto de x
<pre lang="text">
   notation `|`x`|` := abs x

def limite (u: ℕ → ℝ) (a: ℝ) :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

donde se usa la notación |x| para el valor absoluto de x

notation `|`x`|` := abs x

y que la sucesión u es no decreciente por

   def no_decreciente (u : ℕ → ℝ) :=
     ∀ n m, n ≤ m → u n ≤ u m

1 2	def no_decreciente (u : ℕ → ℝ) := ∀ n m, n ≤ m → u n ≤ u m

Demostrar que si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n.

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

import data.real.basic
import tactic

variable {u : ℕ → ℝ}
variable (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m

example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
sorry

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

variable (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def no_decreciente (u : ℕ → ℝ) :=

∀ n m, n ≤ m → u n ≤ u m

example

(h : limite u a)

(h' : no_decreciente u)

: ∀ n, u n ≤ a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variable {u : ℕ → ℝ}
variable (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m

-- 1ª demostración
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
begin
  intro n,
  by_contradiction H,
  push_neg at H,
  replace H : u n - a > 0 := sub_pos.mpr H,
  cases h (u n - a) H with m hm,
  let k := max n m,
  specialize hm k (le_max_right _ _),
  specialize h' n k (le_max_left _ _),
  replace hm : |u k - a| < u k - a, by
    calc |u k - a| < u n - a : hm
               ... ≤ u k - a : sub_le_sub_right h' a,
  rw ← not_le at hm,
  apply hm,
  exact le_abs_self (u k - a),
end

-- 2ª demostración
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
begin
  intro n,
  by_contradiction H,
  push_neg at H,
  cases h (u n - a) (by linarith) with m hm,
  specialize hm (max n m) (le_max_right _ _),
  specialize h' n (max n m) (le_max_left _ _),
  rw abs_lt at hm,
  linarith,
end

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

variable (a : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε

def no_decreciente (u : ℕ → ℝ) :=

∀ n m, n ≤ m → u n ≤ u m

-- 1ª demostración

example

(h : limite u a)

(h' : no_decreciente u)

: ∀ n, u n ≤ a :=

begin

intro n,

by_contradiction H,

push_neg at H,

replace H : u n - a > 0 := sub_pos.mpr H,

cases h (u n - a) H with m hm,

let k := max n m,

specialize hm k (le_max_right _ _),

specialize h' n k (le_max_left _ _),

replace hm : |u k - a| < u k - a, by

calc |u k - a| < u n - a : hm

... ≤ u k - a : sub_le_sub_right h' a,

rw ← not_le at hm,

apply hm,

exact le_abs_self (u k - a),

end

-- 2ª demostración

example

(h : limite u a)

(h' : no_decreciente u)

: ∀ n, u n ≤ a :=

begin

intro n,

by_contradiction H,

push_neg at H,

cases h (u n - a) (by linarith) with m hm,

specialize hm (max n m) (le_max_right _ _),

specialize h' n (max n m) (le_max_left _ _),

rw abs_lt at hm,

linarith,

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Limite_de_sucesiones_no_decrecientes
imports Main HOL.Real
begin

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

definition no_decreciente :: "(nat ⇒ real) ⇒ bool"
  where "no_decreciente u ⟷ (∀ n m. n ≤ m ⟶ u n ≤ u m)"

(* 1ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have "a < u n"
      by (rule not_le_imp_less)
    then have H : "u n - a > 0"
      by (simp only: diff_gt_0_iff_gt)
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "n ≤ ?k"
      by (simp only: assms(2) no_decreciente_def)
    then have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by blast
    have "¦u ?k - a¦ < u n - a"
      by (simp only: hm)
    also have "… ≤ u ?k - a"
      using ‹u n ≤ u ?k› by (rule diff_right_mono)
    finally have "¦u ?k - a¦ < u ?k - a"
      by this
    then have "¬ u ?k - a ≤ ¦u ?k - a¦"
      by (simp only: not_le_imp_less)
    moreover have "u ?k - a ≤ ¦u ?k - a¦"
      by (rule abs_ge_self)
    ultimately show False
      by (rule notE)
  qed
qed

(* 2ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have H : "u n - a > 0"
      by simp
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately have "¦u ?k - a¦ < u ?k - a"
      by simp
    then show False
      by simp
  qed
qed

(* 3ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by fastforce
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately show False
      by simp
  qed
qed

end

theory Limite_de_sucesiones_no_decrecientes

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition no_decreciente :: "(nat ⇒ real) ⇒ bool"

where "no_decreciente u ⟷ (∀ n m. n ≤ m ⟶ u n ≤ u m)"

(* 1ª demostración *)

lemma

assumes "limite u a"

"no_decreciente u"

shows "∀ n. u n ≤ a"

proof (rule allI)

fix n

show "u n ≤ a"

proof (rule ccontr)

assume "¬ u n ≤ a"

then have "a < u n"

by (rule not_le_imp_less)

then have H : "u n - a > 0"

by (simp only: diff_gt_0_iff_gt)

then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"

using assms(1) limite_def by blast

let ?k = "max n m"

have "n ≤ ?k"

by (simp only: assms(2) no_decreciente_def)

then have "u n ≤ u ?k"

using assms(2) no_decreciente_def by blast

have "¦u ?k - a¦ < u n - a"

by (simp only: hm)

also have "… ≤ u ?k - a"

using ‹u n ≤ u ?k› by (rule diff_right_mono)

finally have "¦u ?k - a¦ < u ?k - a"

by this

then have "¬ u ?k - a ≤ ¦u ?k - a¦"

by (simp only: not_le_imp_less)

moreover have "u ?k - a ≤ ¦u ?k - a¦"

by (rule abs_ge_self)

ultimately show False

by (rule notE)

qed

(* 2ª demostración *)

lemma

assumes "limite u a"

"no_decreciente u"

shows "∀ n. u n ≤ a"

proof (rule allI)

fix n

show "u n ≤ a"

proof (rule ccontr)

assume "¬ u n ≤ a"

then have H : "u n - a > 0"

by simp

then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"

using assms(1) limite_def by blast

let ?k = "max n m"

have "¦u ?k - a¦ < u n - a"

using hm by simp

moreover have "u n ≤ u ?k"

using assms(2) no_decreciente_def by simp

ultimately have "¦u ?k - a¦ < u ?k - a"

by simp

then show False

by simp

qed

(* 3ª demostración *)

lemma

assumes "limite u a"

"no_decreciente u"

shows "∀ n. u n ≤ a"

proof

fix n

show "u n ≤ a"

proof (rule ccontr)

assume "¬ u n ≤ a"

then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"

using assms(1) limite_def by fastforce

let ?k = "max n m"

have "¦u ?k - a¦ < u n - a"

using hm by simp

moreover have "u n ≤ u ?k"

using assms(2) no_decreciente_def by simp

ultimately show False

by simp

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]