Demostrar que si la sucesión \(a\) converge a \(L\), entonces \[ (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1] \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a : ℕ → ℝ} variable {L : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) : ∃ N, ∀ n ≥ N, a n ≥ L - 1 := by sorry
Demostrar que si \(aₙ\) converge a \(L\) y \(bₙ\) a \(M\), entonces \(aₙ+bₙ\) converge a \(L+M\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {a b c : ℕ → ℝ} variable {L M : ℝ} def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hb : SeqLim b M) : SeqLim (a + b) (L + M) := by sorry
El reto de esta semana consiste en demostrar con Lean 4 que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry
El reto de esta semana consiste en demostrar con Lean 4 que si la sucesión \(aₙ\) converge a \(L\), entonces \(2aₙ\) converge a \(2L\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a : ℕ → ℝ) def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε example (ha : SeqLim a L) (hb : ∀ n, b n = 2 * a n) : SeqLim b (2 * L) := by sorry
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 SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε def SucConv (a : ℕ → ℝ) : Prop := ∃ L, SeqLim a L example (ha : ∀ n, a n = (-1) ^ n) : ¬ SucConv a := by sorry
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 SeqLim (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 SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε example (ha : ∀ n, a n = 1 / n) : SeqLim a 0 := by sorry
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.
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
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
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