Skip to main content

Si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n

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_n\).

En Lean4, 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| < ε

y que la sucesión \(u\) es no decreciente por

   def no_decreciente (u : ℕ → ℝ) :=
     ∀ n m, n ≤ m → u n ≤ u m

Demostrar con Lean4 que si \(u\) es una sucesión no decreciente y su límite es \(a\), entonces \(u(n) ≤ a\) para todo \(n\).

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

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

variable {u : ℕ → ℝ}
variable (a : ℝ)

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

def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m

example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
by sorry

1. Demostración en lenguaje natural

Lo demostraremos por reducción al absurdo. Para ello, sea \(n ∈ ℕ\) tal que \[ a < u(n) \] Entonces, \[ u(n) - a > 0 \] y, puesto que \(a\) es límite de \(u\), existe un \(m ∈ ℕ\) tal que \[ (∀ n' ≥ m)[|u(n') - a| < u(n) - a] \tag{1} \] Sea \(k = \max(n, m)\). Entonces, \begin{align} k &≥ n \tag{2} \newline k &≥ m \tag{3} \end{align} Por (1) y (3) se tiene que \[ |u(k) - a| < u(n) - a \tag{4} \] Por (2), puesto que \(u\) es no decreciente, se tiene que \[ u(n) ≤ u(k) \tag{5} \] Por tanto, \begin{align} u(k) - a &≤ |u(k) - a| \newline &< u(n) - a &&\text{[por (4)]} \newline &≤ u(k) - a &&\text{[por (5)]} \end{align} Luego, \[ u(k) - a < u(k) - a \] que es una contradicción.

2. Demostraciones con Lean4

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

variable {u : ℕ → ℝ}
variable (a : ℝ)

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

def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m

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

example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
by
  intro n
  -- n : ℕ
  -- ⊢ u n ≤ a
  by_contra H
  -- H : ¬u n ≤ a
  -- ⊢ False
  push_neg at H
  -- H : a < u n
  replace H : u n - a > 0 := sub_pos.mpr H
  cases' h (u n - a) H with m hm
  -- m : ℕ
  -- hm : ∀ (n_1 : ℕ), n_1 ≥ m → |u n_1 - a| < u n - a
  let k := max n m
  have h1 : k ≥ n := le_max_left n m
  have h2 : k ≥ m := le_max_right n m
  have h3 : u k - a < u k - a := by
    calc u k  - a ≤ |u k - a| := by exact le_abs_self (u k - a)
                _ < u n - a   := hm k h2
                _ ≤ u k - a   := sub_le_sub_right (h' n k h1) a
  exact gt_irrefl (u k - a) h3

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

example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
by
  intro n
  -- n : ℕ
  -- ⊢ u n ≤ a
  by_contra H
  -- H : ¬u n ≤ a
  -- ⊢ False
  push_neg at H
  -- H : a < u n
  replace H : u n - a > 0 := sub_pos.mpr H
  cases' h (u n - a) H with m hm
  -- m : ℕ
  -- hm : ∀ (n_1 : ℕ), n_1 ≥ m → |u n_1 - a| < u n - a
  let k := max n m
  specialize hm k (le_max_right _ _)
  -- hm : |u k - a| < u n - a
  specialize h' n k (le_max_left _ _)
  -- h' : u n ≤ u k
  replace hm : |u k - a| < u k - a := by
    calc |u k - a| < u n - a := by exact hm
                 _ ≤ u k - a := sub_le_sub_right h' a
  rw [← not_le] at hm
  -- hm : ¬u k - a ≤ |u k - a|
  apply hm
  -- ⊢ u k - a ≤ |u k - a|
  exact le_abs_self (u k - a)

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

example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
by
  intro n
  -- n : ℕ
  -- ⊢ u n ≤ a
  by_contra H
  -- H : ¬u n ≤ a
  -- ⊢ False
  push_neg at H
  -- H : a < u n
  cases' h (u n - a) (by linarith) with m hm
  -- m : ℕ
  -- hm : ∀ (n_1 : ℕ), n_1 ≥ m → |u n_1 - a| < u n - a
  specialize hm (max n m) (le_max_right _ _)
  -- hm : |u (max n m) - a| < u n - a
  specialize h' n (max n m) (le_max_left _ _)
  -- h' : u n ≤ u (max n m)
  rw [abs_lt] at hm
  -- hm : -(u n - a) < u (max n m) - a ∧ u (max n m) - a < u n - a
  linarith

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

-- variable (b : ℝ)
-- #check (abs_lt: |a| < b ↔ -b < a ∧ a < b)
-- #check (gt_irrefl a : ¬(a > a))
-- #check (le_abs_self a : a ≤ |a|)
-- #check (le_max_left a b : a ≤ max a b)
-- #check (le_max_right a b : b ≤ max a b)
-- #check (sub_le_sub_right : a ≤ b → ∀ (c : ℝ), a - c ≤ b - c)
-- #check (sub_pos : 0 < a - b ↔ b < a)

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

3. Demostraciones con Isabelle/HOL

theory Limite_de_sucesiones_no_decrecientes
imports Main HOL.Real
begin

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

definition no_decreciente :: "(nat ⇒ real) ⇒ bool"
  where "no_decreciente u ⟷ (∀ n m. n ≤ m ⟶ u n ≤ u m)"

(* 1ª demostración *)

lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have "a < u n"
      by (rule not_le_imp_less)
    then have H : "u n - a > 0"
      by (simp only: diff_gt_0_iff_gt)
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "n ≤ ?k"
      by (simp only: assms(2) no_decreciente_def)
    then have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by blast
    have "¦u ?k - a¦ < u n - a"
      by (simp only: hm)
    also have "… ≤ u ?k - a"
      using ‹u n ≤ u ?k› by (rule diff_right_mono)
    finally have "¦u ?k - a¦ < u ?k - a"
      by this
    then have "¬ u ?k - a ≤ ¦u ?k - a¦"
      by (simp only: not_le_imp_less)
    moreover have "u ?k - a ≤ ¦u ?k - a¦"
      by (rule abs_ge_self)
    ultimately show False
      by (rule notE)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have H : "u n - a > 0"
      by simp
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately have "¦u ?k - a¦ < u ?k - a"
      by simp
    then show False
      by simp
  qed
qed

(* 3ª demostración *)

lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by fastforce
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately show False
      by simp
  qed
qed

end