Ir al contenido principal

Publicaciones sobre ITP

Canal RSS (ITP, es)

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

Retos en Lean 4

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

¿Cómo publicar tu solución?

  1. Escribe tu demostración en live.lean-lang.org y copia el enlace que genera.
  2. Publícalo en el hilo de Mastodon de este problema, con un mensaje del tipo:
    «Mi solución está en [enlace].»
  3. Podrás comparar tu planteamiento con el de otros participantes durante la semana. La solución oficial se publicará el próximo lunes.

Reto 22: Subsucesiones con límites distintos implican no convergencia

Retos en Lean 4

Demostrar que si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente.

Para ello, completar la siguiente teoría:

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

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

-- La sucesión a es convergente
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ es una función de extracción.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b es una subsucesión de a.
def Subseq (b a : ℕ → ℝ) : Prop :=
  ∃ φ, IsExtraction φ ∧ b = a ∘ φ

variable {a b₁ b₂ : ℕ → ℝ}
variable {L L₁ L₂ : ℝ}

example
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SeqConv a :=
by sorry

Leer más…

Reto 21: Las subsucesiones tienen el mismo límite que la sucesión

Retos en Lean 4

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

Leer más…

Reto 20: Si aₙ → L y M es una cota superior de aₙ, entonces L ≤ M

Retos en Lean 4

Demostrar que si la sucesión \(a_{n}\) converge a \(L\) y \(M\) es una cota superior de \(a_{n}\) (es decir, \(a_{n} ≤ M\) para todo \(n\)), entonces \(L ≤ M\).

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

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

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

def IsUB (a : ℕ → ℝ) (M : ℝ) : Prop :=
  ∀ n, a n ≤ M

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

example
  (ha : SeqLim a L)
  (hM : IsUB a M)
  : L ≤ M :=
by sorry

Leer más…

Reto 19: Las sucesiones convergentes son sucesiones de Cauchy

Retos en Lean 4

Demostrar que las sucesiones convergentes son sucesiones de Cauchy

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

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

variable {u : ℕ → ℝ}

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

def SeqConv (u : ℕ → ℝ) :=
  ∃ a, SeqLim u a

def IsCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

example
  (h : SeqConv u)
  : IsCauchy u :=
by sorry

Leer más…

Reto 18: Convergencia del producto de sucesiones convergentes

Retos en Lean 4

El reto de esta semana consiste en demostrar en Lean 4 que si la sucesión \(aₙ\) converge a \(L\) y \(bₙ\) converge a \(M\), entonces \(aₙbₙ\) converge a \(LM\).

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

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

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

variable {a b c : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hc : ∀ n, c n = a n * b n)
  : SeqLim c (L * M) :=
by sorry

Leer más…

Reto 17: Las sucesiones convergentes están acotadas

Retos en Lean 4

El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión \(a_n\) es convergente, entonces \(a_n\) está acotada; es decir, existe un \(M ∈ ℝ\) tal que para todo \(n ∈ ℕ\), \(|a_n| ≤ M\).

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

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

open Finset

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

def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

def SeqBdd (a : ℕ → ℝ) : Prop :=
  ∃ M, ∀ n, |a n| ≤ M

variable (a : ℕ → ℝ)

example
  (ha : SeqConv a)
  : SeqBdd a :=
by sorry

Leer más…