Ir al contenido principal

Publicaciones sobre Límites (publicaciones antiguas, página 1)

Canal RSS (Límites, es)

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…

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

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

Demostrar el teorema del emparedado; es decir que si \(a_n\) y \(c_n\) convergen a \(L\) y \(a_n ≤ b_n \leq c_n\) para todo \(n\), entonces \(b_n\) 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 SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

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

Leer más…

Reto 3: Si aₙ converge a L, entonces 2aₙ converge a 2L

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

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

Leer más…

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

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

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 SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

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

Leer más…

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

Retos en Lean 4/Análisis/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 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

Leer más…