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

José A. Alonso

06-06-2024

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

1. Demostración en lenguaje natural

Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que \[ (∃ N ∈ ℕ)(∀ n ≥ N)[|-u_n - -a| < ε] \tag{1} \] Puesto que el límite de \(u_n\) es \(a\), existe un \(k ∈ ℕ\) tal que \[ (∀ n ≥ k)[|u_n - a| < ε] \tag{2} \] Veamos que con \(k\) se cumple (1). En efecto, sea \(n ≥ k\). Entonces, \begin{align} |-u_n - -a| &= |-(u_n - a)| \newline &= |u_n - a| \newline &< ε &&\text{[por (2)]} \end{align}

2. Demostraciones con 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| < ε

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

example
  (h : limite u a)
  : limite (fun n ↦ -u n) (-a) :=
by
  unfold limite at *
  -- h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε
  -- ⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => -u n) n - -a| < ε
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => -u n) n - -a| < ε
  specialize h ε hε
  -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε
  cases' h with k hk
  -- k : ℕ
  -- hk : ∀ (n : ℕ), n ≥ k → |u n - a| < ε
  use k
  -- ⊢ ∀ (n : ℕ), n ≥ k → |(fun n => -u n) n - -a| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |(fun n => -u n) n - -a| < ε
  calc |(fun n => -u n) n - -a|
       = |(-u n - -a)|          := rfl
     _ = |(-(u n - a))|         := by congr ; ring
     _ = |(u n - a)|            := abs_neg (u n - a)
     _ < ε                      := hk n hn

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

example
  (h : limite u a)
  : limite (fun n ↦ -u n) (-a) :=
by
  unfold limite at *
  -- h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε
  -- ⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => -u n) n - -a| < ε
  have h1 : ∀ n, |u n - a| = |(-u n - -a)| := by
    intro n
    -- n : ℕ
    -- ⊢ |u n - a| = |-u n - -a|
    rw [abs_sub_comm]
    -- ⊢ |a - u n| = |-u n - -a|
    congr 1
    -- ⊢ a - u n = -u n - -a
    ring
  simpa [h1] using h

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

-- variable (b : ℝ)
-- #check (abs_neg a : |(-a)| = |a|)
-- #check (abs_sub_comm a b : |a - b| = |b - a|)

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

3. Demostraciones con Isabelle/HOL

theory Limite_de_la_opuesta
imports Main HOL.Real
begin

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

(* 1ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦-u n - -a¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"
      using assms limite_def
      by auto
    have "∀n≥N. ¦-u n - -a¦ < ε"
      proof (intro allI impI)
        fix n
        assume "n ≥ N"
        have "¦-u n - -a¦ = ¦u n - a¦"
          by argo
        also have "… < ε"
          using hN ‹n ≥ N›
          by simp
        finally show "¦-u n - -a¦ < ε"
          by simp
    qed
    then show "∃k. ∀n≥k. ¦-u n - -a¦ < ε"
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦-u n - -a¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"
      using assms limite_def
      by auto
    have "∀n≥N. ¦-u n - -a¦ < ε"
      using hN by fastforce
    then show "∃k. ∀n≥k. ¦-u n - -a¦ < ε"
      by (rule exI)
  qed
qed

(* 3ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦-u n - -a¦ < ε"
    using assms limite_def by force
qed

(* 4ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
using assms limite_def by force

end