Skip to main content

Reto 12: Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ

El reto de esta semana consiste en demostrar en Lean 4 que si las sucesiones \(a_n\) y \(b_n\) convergen a \(L\) y \(M\), respectivamente, con \(L < M\), entonces eventualmente \(a_n < b_n\); es decir, que existe un \(k ∈ \mathbb{N}\) tal que, para todo \(n ≥ k\), \(a_n < b_n\).

Para ello, completar la siguiente teoría de Lean 4:

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

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

variable {a b : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by sorry

1. Demostración en lenguaje natural

Sea \[ \varepsilon = \dfrac{M - L}{2} \tag{1} \]

Puesto que \(L < M\), se tiene que \(\varepsilon > 0\). Y, usando las convergencias de \(a_n\) y \(b_n\), se tiene que existen \(k_1\) y \(k_2\) tales que \[ \forall n ≥ k_1, |a_n - L| < \varepsilon \tag{2} \] \[ \forall n ≥ k_2, |b_n - M| < \varepsilon \tag{3} \] Sea \[ k = \max(k_1, k_2) \tag{4} \] Veamos que \[ \forall n \geq k, a_n < b_n \] Para ello, sea \(n ∈ \mathbb{N}\) tal que \[ n \geq k \tag{5} \] Entonces, por (4) y (5), se tiene que \[ n \geq k_1 \] Luego, por (2), se tiene que \[ |a_n - L| < \varepsilon \] y, por consiguiente, \[ a_n - L < \varepsilon \tag{6} \]

También, por (4) y (5), se tiene que \[ n \geq k_2 \] Luego, por (3), se tiene que \[ |b_n - M| < \varepsilon \] y, por consiguiente, \[ -\varepsilon < b_n - M \tag{7} \]

Finalmente, \[ \begin{array}{llll} a_n &< \varepsilon + L &&\text{[por (6)]} \\ &= \dfrac{M - L}{2} + L &&\text{[por (1)]} \\ &= \dfrac{L + M}{2} \\ &= -\left(\dfrac{M - L}{2}\right) + M \\ &= -\varepsilon + M &&\text{[por (1)]} \\ &< b_n &&\text{[por (7)]} \\ \end{array} \]

2. Demostraciones con Lean4

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

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

variable {a b : ℕ → ℝ}
variable {L M : ℝ}

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

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by grind)
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε (by grind)
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  use max k1 k2
  -- ⊢ ∀ n ≥ max k1 k2, a n < b n
  grind

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

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by grind)
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε (by grind)
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  use max k1 k2
  -- ⊢ ∀ n ≥ max k1 k2, a n < b n
  intro n hn
  -- n : ℕ
  -- hn : n ≥ max k1 k2
  -- ⊢ a n < b n
  calc
    a n
    < ε + L              := by grind
  _ = (M - L) / 2 + L    := by grind
  _ = (L + M) / 2        := by grind
  _ = -((M - L) / 2) + M := by grind
  _ = -ε + M             := by grind
  _ < b n                := by grind

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

example
    (ha : LimSuc a L)
    (hb : LimSuc b M)
    (hLM : L < M) :
    ∃ k, ∀ n ≥ k, a n < b n := by
  set ε := (M - L) / 2 with ε_def
  -- ε_def : ε = (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by positivity)
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε (by positivity)
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  set k := max k1 k2
  use k
  -- ⊢ ∀ n ≥ k, a n < b n
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ a n < b n
  have h1 : n ≥ k1 := le_of_max_le_left hn
  have h2 : |a n - L| < ε := hk1 n h1
  have h3 : a n - L < ε := lt_of_abs_lt h2
  have h4 : n ≥ k2 := le_of_max_le_right hn
  have h5 : |b n - M| < ε := hk2 n h4
  have h6 : -ε < b n - M := neg_lt_of_abs_lt h5
  calc
    a n
    < ε + L              := lt_add_of_tsub_lt_right h3
  _ = (M - L) / 2 + L    := by rw [ε_def]
  _ = (L + M) / 2        := by ring
  _ = -((M - L) / 2) + M := by ring
  _ = -ε + M             := by rw [ε_def]
  _ < b n                := lt_tsub_iff_right.mp h6

-- 4ª demostración
-- ===============

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2 with ε_def
  -- ε_def : ε = (M - L) / 2
  have hε : ε > 0 := half_pos (sub_pos_of_lt hLM)
  obtain ⟨k1, hk1⟩ := ha ε hε
  -- k1 : ℕ
  -- hk1 : ∀ n ≥ k1, |a n - L| < ε
  obtain ⟨k2, hk2⟩ := hb ε hε
  -- k2 : ℕ
  -- hk2 : ∀ n ≥ k2, |b n - M| < ε
  set k := max k1 k2
  use k
  -- ⊢ ∀ n ≥ k, a n < b n
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ a n < b n
  have h1 : n ≥ k1 := le_of_max_le_left hn
  have h2 : |a n - L| < ε := hk1 n h1
  have h3 : a n - L < ε := lt_of_abs_lt h2
  have h4 : n ≥ k2 := le_of_max_le_right hn
  have h5 : |b n - M| < ε := hk2 n h4
  have h6 : -ε < b n - M := neg_lt_of_abs_lt h5
  calc
    a n
    < ε + L              := lt_add_of_tsub_lt_right h3
  _ = (M - L) / 2 + L    := congrArg (· + L) ε_def
  _ = (L + M) / 2        := by ring
  _ = -((M - L) / 2) + M := by ring
  _ = -ε + M             := congrArg (-· + M) ε_def
  _ < b n                := lt_tsub_iff_right.mp h6

-- 5ª demostración
-- ===============

example
  (ha : LimSuc a L)
  (hb : LimSuc b M)
  (hLM : L < M)
  : ∃ k, ∀ n ≥ k, a n < b n :=
by
  set ε := (M - L) / 2
  obtain ⟨k1, hk1⟩ := ha ε (by grind)
  obtain ⟨k2, hk2⟩ := hb ε (by grind)
  exact ⟨max k1 k2, fun _ _ => by grind⟩

En el siguiente vídeo se explica paso a paso la construcción de las soluciones:

Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.