Skip to content

Latest commit

 

History

History
263 lines (227 loc) · 7.1 KB

Las_sucesiones_divergentes_positivas_no_tienen_limites_finitos.md

File metadata and controls

263 lines (227 loc) · 7.1 KB
Raw
title date category has_math
Las sucesiones divergentes positivas no_tienen límites finitos
2024-07-26 06:00:00 UTC+02:00
Límites
true

[mathjax]

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 que \(a\) es el límite de la sucesión \(u\), por

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

La sucesión \(u\) diverge positivamente cuando, para cada número real \(A\), se puede encontrar un número natural \(m\) tal que si \(n ≥ m\), entonces \(uₙ > A\). En Lean se puede definir por

   def diverge_positivamente (u : ℕ → ℝ) :=
     ∀ A, ∃ m, ∀ n ≥ m, u n > A

Demostrar que si \(u\) diverge positivamente, entonces ningún número real es límite de \(u\).

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

import Mathlib.Data.Real.Basic

variable {u : ℕ → ℝ}

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

def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
by sorry

1. Demostración en lenguaje natural

Supongamos que existe un \(a ∈ ℝ\) tal que \(a\) es límite de \(u\). Entonces, existe un \(m_1 ∈ ℕ\) tal que \[ (∀ n ≥ m_1) |u_n - a| < 1 \tag{1} \] Puesto que \(u\) diverge positivamente, existe un \(m_2 ∈ ℕ\) tal que \[ (∀ n ≥ m_2) u_n > a + 1 \tag{2} \] Sea \(m\) el máximo de \(m_1\) y \(m_2\). Entonces, \begin{align} m &≥ m_1 \tag{3} \\ m &≥ m_2 \tag{4} \end{align} Por (1) y (3), se tiene que \[ |u_m - a| < 1 \] Luego, \[ u_m - a < 1 \tag{5} \] Por (2) y (4), se tiene que \[ u_m > a + 1 \tag{6} \] Por tanto, \begin{align} u_m &< a + 1 &&\text{[por (5)]} \\ &< u_m &&\text{[por (6)]} \end{align} De donde se tiene que \[ u_m < u_m \] que es una contradicción.

2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable {u : ℕ → ℝ}

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

def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A

-- 1ª demostración
-- ===============

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
by
  push_neg
  -- ⊢ ∀ (a : ℝ), ¬limite u a
  intros a ha
  -- a : ℝ
  -- ha : limite u a
  -- ⊢ False
  cases' ha 1 zero_lt_one with m1 hm1
  -- m1 : ℕ
  -- hm1 : ∀ (n : ℕ), n ≥ m1 → |u n - a| < 1
  cases' h (a+1) with m2 hm2
  -- m2 : ℕ
  -- hm2 : ∀ (n : ℕ), n ≥ m2 → u n > a + 1
  let m := max m1 m2
  specialize hm1 m (le_max_left _ _)
  -- hm1 : |u m - a| < 1
  specialize hm2 m (le_max_right _ _)
  -- hm2 : u m > a + 1
  replace hm1 : u m - a < 1 := lt_of_abs_lt hm1
  replace hm2 : 1 < u m - a := lt_sub_iff_add_lt'.mpr hm2
  apply lt_irrefl (u m)
  -- ⊢ u m < u m
  calc u m < a + 1 := by exact sub_lt_iff_lt_add'.mp hm1
         _ < u m   := lt_sub_iff_add_lt'.mp hm2

-- 2ª demostración
-- ===============

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
by
  push_neg
  -- ⊢ ∀ (a : ℝ), ¬limite u a
  intros a ha
  -- a : ℝ
  -- ha : limite u a
  -- ⊢ False
  cases' ha 1 (by linarith) with m1 hm1
  -- m1 : ℕ
  -- hm1 : ∀ (n : ℕ), n ≥ m1 → |u n - a| < 1
  cases' h (a+1) with m2 hm2
  -- m2 : ℕ
  -- hm2 : ∀ (n : ℕ), n ≥ m2 → u n > a + 1
  let m := max m1 m2
  replace hm1 : |u m - a| < 1 := by aesop
  replace hm1 : u m - a < 1   := lt_of_abs_lt hm1
  replace hm2 : a + 1 < u m   := by aesop
  replace hm2 : 1 < u m - a   := lt_sub_iff_add_lt'.mpr hm2
  apply lt_irrefl (u m)
  -- ⊢ u m < u m
  calc u m < a + 1 := by linarith
         _ < u m   := by linarith

-- 3ª demostración
-- ===============

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
by
  push_neg
  -- ⊢ ∀ (a : ℝ), ¬limite u a
  intros a ha
  -- a : ℝ
  -- ha : limite u a
  -- ⊢ False
  cases' ha 1 (by linarith) with m1 hm1
  -- m1 : ℕ
  -- hm1 : ∀ (n : ℕ), n ≥ m1 → |u n - a| < 1
  cases' h (a+1) with m2 hm2
  -- m2 : ℕ
  -- hm2 : ∀ (n : ℕ), n ≥ m2 → u n > a + 1
  let m := max m1 m2
  specialize hm1 m (le_max_left _ _)
  -- hm1 : |u m - a| < 1
  rw [abs_lt] at hm1
  -- hm1 : -1 < u m - a ∧ u m - a < 1
  specialize hm2 m (le_max_right _ _)
  -- hm2 : u m > a + 1
  linarith

-- Lemas usados
-- ============

-- variable (m n : ℕ)
-- variable (a b c : ℝ)
-- #check (abs_lt: |a| < b ↔ -b < a ∧ a < b)
-- #check (le_max_left m n : m ≤ max m n)
-- #check (le_max_right m n : n ≤ max m n)
-- #check (lt_irrefl a : ¬a < a)
-- #check (lt_of_abs_lt : |a| < b → a < b)
-- #check (lt_sub_iff_add_lt' : b < c - a ↔ a + b < c)
-- #check (sub_lt_iff_lt_add' : a - b < c ↔ a < b + c)
-- #check (zero_lt_one : 0 < 1)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory Las_sucesiones_divergentes_positivas_no_tienen_limites_finitos
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition diverge_positivamente :: "(nat ⇒ real) ⇒ bool"
  where "diverge_positivamente u ⟷ (∀A. ∃m. ∀n≥m. u n > A)"

(* 1ª demostración *)

lemma
  assumes "diverge_positivamente u"
  shows   "∄a. limite u a"
proof (rule notI)
  assume "∃a. limite u a"
  then obtain a where "limite u a" try
    by auto
  then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"
    using limite_def by fastforce
  obtain m2 where hm2 : "∀n≥m2. u n > a + 1"
    using assms diverge_positivamente_def by blast
  let ?m = "max m1 m2"
  have "u ?m < u ?m" using hm1 hm2
  proof -
    have "?m ≥ m1"
      by (rule max.cobounded1)
    have "?m ≥ m2"
      by (rule max.cobounded2)
    have "u ?m - a < 1"
      using hm1 ‹?m ≥ m1› by fastforce
    moreover have "u ?m > a + 1"
      using hm2 ‹?m ≥ m2› by simp
    ultimately show "u ?m < u ?m"
      by simp
  qed
  then show False
    by auto
qed

(* 2ª demostración *)

lemma
  assumes "diverge_positivamente u"
  shows   "∄a. limite u a"
proof (rule notI)
  assume "∃a. limite u a"
  then obtain a where "limite u a" try
    by auto
  then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"
    using limite_def by fastforce
  obtain m2 where hm2 : "∀n≥m2. u n > a + 1"
    using assms diverge_positivamente_def by blast
  let ?m = "max m1 m2"
  have "1 < 1"
  proof -
    have "1 < u ?m - a"
      using hm2
      by (metis add.commute less_diff_eq max.cobounded2)
    also have "… < 1"
      using hm1
      by (metis abs_less_iff max_def order_refl)
    finally show "1 < 1" .
  qed
  then show False
    by auto
qed

end