Ir al contenido principal

Publicaciones sobre Análisis (publicaciones antiguas, página 1)

Subcategorías:

RSS feed (Analysis, en)

Canal RSS (Análisis, es)

También disponible en:

English (Analysis)

Las funciones de extracción no están acotadas

Análisis/Sucesiones

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(ϕ\) tal que \(ϕ(n) = 2n\).

En Lean4, se puede definir que \(ϕ\) es una función de extracción por

   def extraccion (ϕ : ℕ → ℕ) :=
     ∀ n m, n < m → ϕ n < ϕ m

Demostrar que las funciones de extracción no están acotadas; es decir, que si \(ϕ\) es una función de extracción, entonces \[ (∀ N, N')(∃ n ≥ N')[ϕ(n) ≥ N] \]

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

import Mathlib.Tactic
open Nat

variable {ϕ : ℕ → ℕ}

def extraccion (ϕ : ℕ → ℕ) :=
  ∀ n m, n < m → ϕ n < ϕ m

example
  (h : extraccion ϕ)
  : ∀ N N', ∃ n ≥ N', ϕ n ≥ N :=
by sorry

Leer más…

Relación entre los índices de las subsucesiones y de la sucesión

Análisis/Sucesiones

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(ϕ\) tal que \(ϕ(n) = 2n\).

En Lean4, se puede definir que \(ϕ\) es una función de extracción por

   def extraccion (ϕ : ℕ → ℕ) :=
     ∀ {n m}, n < m → ϕ n < ϕ m

Demostrarcon Lean4 que si \(ϕ\) es una función de extracción, entonces \[ (∀ n)[n ≤ ϕ(n) \]

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

import Mathlib.Tactic
open Nat

variable {ϕ : ℕ → ℕ}

def extraccion (ϕ : ℕ → ℕ) :=
  ∀ {n m}, n < m → ϕ n < ϕ m

example :
  extraccion ϕ → ∀ n, n ≤ ϕ n :=
by sorry

Leer más…

Las sucesiones convergentes son sucesiones de Cauchy

Análisis/Límites

En Lean4, una sucesión \(u_0, u_1, u_2, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(uₙ\).

Se define

  • \(a\) es un límite de la sucesión \(u\) , por
     def limite (u : ℕ → ℝ) (a : ℝ) :=
       ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| ≤ ε
  • la sucesión \(u\) es convergente por
     def suc_convergente (u : ℕ → ℝ) :=
       ∃ a, limite u a
  • la sucesión \(u\) es de Cauchy por
     def suc_Cauchy (u : ℕ → ℝ) :=
       ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

Demostrar con Lean4 que las sucesiones convergentes son de Cauchy.

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

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

variable {u : ℕ → ℝ }

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

def suc_convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

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

example
  (h : suc_convergente u)
  : suc_Cauchy u :=
by sorry

Leer más…

Si el límite de la sucesión uₙ es a, entonces el límite de -uₙ es -a

Análisis/Límites

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

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

   def limite : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

Demostrar con Lean4 que que si el límite de \(u_n\) es \(a\), entonces el de \(-u_n\) es \(-a\).

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

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

variable (u v : ℕ → ℝ)
variable (a c : ℝ)

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (h : limite u a)
  : limite (fun n ↦ -u n) (-a) :=
by sorry

Leer más…

Si uₙ está acotada y el límite de vₙ es 0, entonces el límite de uₙ·vₙ es 0

Análisis/Límites

Demostrar con Lean4 que si \(u_n\) está acotada y el límite de \(v_n\) es \(0\), entonces el límite de \(u_n·v_n\) es \(0\).

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

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

variable (u v : ℕ → ℝ)
variable (a : ℝ)

def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

def acotada (a : ℕ → ℝ) :=
  ∃ B, ∀ n, |a n| ≤ B

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
by sorry

Leer más…

Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ

Análisis/Límites

En Lean4, una sucesión \(u_0, u_1, u_2, \dots\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el \(n\)-ésimo término de la sucesión.

Se define que \(a\) límite de la sucesión \(u\) como sigue

   def limite (u : ℕ → ℝ) (c : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

Demostrar que si \((∀ n)[u_n ≤ v_n]\), \(a\) es límite de \(u_n\) y \(c\) es límite de \(v_n\), entonces \(a ≤ c\).

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

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

variable (u v : ℕ → ℝ)
variable (a c : ℝ)

def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by sorry

Leer más…

Las sucesiones convergentes están acotadas

Análisis/Límites

Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir, \[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]

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

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

variable {u : ℕ → ℝ}

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by sorry

Leer más…

Los supremos de las sucesiones crecientes son sus límites

Análisis/Límites

Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).

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

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

variable (u : ℕ → ℝ)
variable (S : ℝ)

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε

-- (supremo u S) expresa que el supremo de u es S.
def supremo (u : ℕ → ℝ) (S : ℝ) :=
  (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by sorry

Leer más…

Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva

Análisis/Funciones reales

Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que \[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \] entonces \(f\) es inyectiva.

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

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by sorry

Leer más…