Ir al contenido principal

Reto 17: Las sucesiones convergentes están acotadas

Retos en Lean 4/Análisis/Límites

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…

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

Retos en Lean 4/Análisis/Números reales

Demostrar 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

Leer más…

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

Retos en Lean 4/Análisis/Límites

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

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

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

Leer más…

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

Retos en Lean 4/Análisis/Límites

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

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

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

Leer más…

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

Retos en Lean 4/Análisis/Límites

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

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

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

Leer más…

Reto 9: Unicidad del límite

Retos en Lean 4/Análisis/Límites

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

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

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

Leer más…

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

Retos en Lean 4/Análisis/Límites

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

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

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

Leer más…