Skip to main content

Reto 19: Las sucesiones convergentes son sucesiones de Cauchy

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 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 LimSuc (u : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def SucConvergente (u : ℕ → ℝ) :=
  ∃ a, LimSuc u a

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

example
  (h : SucConvergente u)
  : SucCauchy u :=
by sorry

Read more…

Reto 18: Convergencia del producto de sucesiones convergentes

RetosLean4

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

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

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

Read more…

Reto 13: Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 la desigualdad triangular inversa; es decir, que para cualesquiera números reales \(x\) e \(y\), se cumple la siguiente relación: \[ ||x| - |y|| ≤ |x - y| \]

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

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

variable (x y : ℝ)

example : |(|x| - |y|)| ≤ |x - y| :=
by sorry

Read more…

Reto 12: Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 que si las sucesiones \(a_n\) y \(b_n\) convergen a \(L\) y \(M\), respectivamente, con \(L < M\), entonces eventualmente \(a_n < b_n\); es decir, que existe un \(k ∈ \mathbb{N}\) tal que, para todo \(n ≥ k\), \(a_n < b_n\).

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

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

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

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

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by sorry

Read more…

Reto 11: Si aₙ converge a L, entonces |aₙ| converge a |L|

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 que si la sucesión \(a_n\) converge a \(L\), entonces \(|a_n|\) converge a \(|L|\).

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

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

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

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = |a n|)
  : LimSuc b |L| :=
by sorry

Read more…

Reto 10: Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión converge a un límite no nulo, entonces sus términos están eventualmente acotados inferiormente por la mitad del valor absoluto del límite; es decir, si una sucesión \(a_n\) converge a \(L\) con \(L ≠ 0\), entonces existe \(k\) tal que para todo \(n ≥ k\) se tiene que \(|aₙ| ≥ \dfrac{|L|}{2}\).

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

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

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

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

example
  (ha : LimSuc a L)
  (hL : L ≠ 0)
  : ∃ k, ∀ n ≥ k, |a n| ≥ |L| / 2 :=
by sorry

Read more…

Reto 9: Unicidad del límite

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión \(aₙ\) converge tanto a \(L\) como a \(M\), entonces \(L = M\).

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

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

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

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

example
  (hL : LimSuc a L)
  (hM : LimSuc a M)
  : L = M :=
by sorry

Read more…

Reto 8: Sucesiones con infinitos términos grandes no convergen a límites pequeños

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 que que una sucesión que posee infinitos términos con valor absoluto superior a 10 no puede converger a un límite cuyo valor absoluto sea menor que 5.

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

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

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

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

example
  (ha : ∀ k, ∃ n ≥ k, |a n| > 10)
  : ¬ ∃ L, LimSuc a L ∧ |L| < 5 :=
by sorry

Read more…

Reto 7: La composición de funciones inyectivas es inyectiva

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 que la composición de funciones inyectivas es inyectiva.

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

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by sorry

Read more…

Reto 6: Si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L

RetosLean4

El reto de esta semana consiste en demostrar en Lean 4 el teorema del emparedado; es decir que si aₙ y cₙ convergen a L y aₙ ≤ bₙ ≤ cₙ para todo n, entonces bₙ converge a L.

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

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

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

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

example
  (ha : LimSuc a L)
  (hc : LimSuc c L)
  (hab : ∀ n, a n ≤ b n)
  (hbc : ∀ n, b n ≤ c n)
  : LimSuc b L := by
  sorry

Read more…