Skip to main content

Reto 2: La sucesión 1, -1, 1, -1,... no es convergente

RetosLean4

En el reto de esta semana continuamos explorando la convergencia de sucesiones, retomando el trabajo de la semana anterior. El problema consiste en demostrar que la sucesión definida por 1, -1, 1, -1,,,, no converge. Para ello, se propone completar la siguiente demostración en Lean 4:

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

variable {a : ℕ → ℝ}

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

def SucConv (a : ℕ → ℝ) : Prop :=
  ∃ L, LimSuc a L

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SucConv a :=
by sorry

Read more…

Reto 1: La sucesión 1/n converge a 0

RetosLean4

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

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

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

Demostrar que si para todo \(n\), \(aₙ = 1/n\), entonces la sucesión \(a\) converge a 0.

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

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

variable (a : ℕ → ℝ)

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

example
  (ha : ∀ n, a n = 1 / n)
  : LimSuc a 0 :=
by sorry

Read more…

Retos de demostración en Lean 4

RetosLean4

He empezado a publicar la serie de "Retos matemáticos en Lean 4" en el canal de Retos matemáticos de Telegram.

La dinámica es sencilla: cada semana publicaré un problema matemático para que los interesados compartan sus soluciones en Lean 4 dentro del grupo. Aunque el acceso es público y cualquiera puede leer los retos, es necesario unirse al grupo en https://t.me/Retos_Matematicos para publicar soluciones.

Al finalizar de la semana publicaré un enlace a Lean Web con las soluciones del reto, que seguirán el siguiente esquema: en primer lugar, una solución en lenguaje natural; a continuación, varias formalizaciones en Lean 4 empezando por la más automática (generalmente, con grind), siguiendo con otras con tácticas más específicas (como norm_num, ring, positivity, linarith) y terminando con una demostración en que la que dichas tácticas se sustituyen por lemas concretos. Con este proceso de refinamiento sucesivo se buscará que la demostración final se corresponda, en la medida de lo posible con la escrita en lenguaje natural.

Una vez concluido cada reto, publicaré las soluciones en este blog bajo la etiqueta Retos Lean4.

Propiedad arquimediana de los números reales

Números reales

Demostrar la propiedad arquimediana de los números reales; es decir, que para cualquier \(ε ∈ ℝ\) con \(0 < ε\), existe \(N ∈ ℕ\) tal que \(1/ε < N\).

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

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

variable {ε : ℝ}
variable (h : 0 < ε)

example : ∃ (N : ℕ), 1 / ε < N :=
by sorry

Read more…

La sucesión constante aₙ = L converge a L

Límites

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

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

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

Demostrar que si para todo \(n\), \(aₙ = L\), entonces la sucesión \(a\) converge a \(L\).

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

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

variable (a : ℕ → ℝ)
variable (L : ℝ)

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

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

Read more…

Demostraciones de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v] \]

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

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen_inversa
imports Main
begin

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
sorry

end

Read more…

Demostraciones de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen_inversa
imports Main
begin

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
sorry

end

Read more…

Demostraciones de "f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable (α β : Type _)
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen
imports Main
begin

lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v"
sorry

end

Read more…

Demostraciones de "f[s] ∩ t = f[s ∩ f⁻¹[t]]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (t : Set β)

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen
imports Main
begin

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
sorry

end

Read more…

Demostraciones de "f[s] \ f[t] ⊆ f[s \ t]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[f[s] \setminus f[t] ⊆ f[s \setminus t] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

lemma "f ` s - f ` t ⊆ f ` (s - t)"
sorry

end

Read more…