Skip to main content

Si aₙ converge a L, entonces 2aₙ converge a 2L

Demostrar que si aₙ converge a L, entonces 2aₙ converge a 2L.

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

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

variable (a : ℕ → ℝ)

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  sorry

1. Demostración en lenguaje natural

Sea \(b_n\) la sucesión definida por \[ b_n = 2a_n \tag{1} \] Tenemos que demostrar que para cada \(ε > 0\), existe un \(N ∈ ℕ\) tal que \[ ∀ n ≥ N, |b_n - 2L| < ε \tag{2} \] Puesto que \(a_n\) converge a \(L\), existe un \(N ∈ ℕ\) tal que \[ ∀ n ≥ N, |a_n - L| < ε/2 \tag{3} \] Veamos que \(N\) también cumple (2). En efecto, sea \(n ≥ N\). Entonces \begin{align} |b_n - 2L| &= |2a_n - 2L| &\text{[por (1)]} \newline &= 2|a_n - L| \newline &< 2ε/2 &\text{[por (3)]} \newline &= ε \newline \end{align}

2. Demostraciones en Lean 4

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

variable {a : ℕ → ℝ}

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

def SucConv (a : ℕ → ℝ) : Prop :=
  ∃ L, LimSuc a L

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain  ⟨N, hN⟩ := ha (ε / 2) (by grind)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  use N
  -- ⊢ ∀ n ≥ N, |b n - 2 * L| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |b n - 2 * L| < ε
  grind

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain  ⟨N, hN⟩ := ha (ε / 2) (by grind)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  use N
  -- ⊢ ∀ n ≥ N, |b n - 2 * L| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |b n - 2 * L| < ε
  calc |b n - 2 * L|
       = |2 * a n - 2 * L| := by grind
     _ = |2 * (a n - L)|   := by grind
     _ = 2 * |a n - L|     := by grind
     _ < 2 * ε / 2         := by grind
     _ = ε                 := by grind

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain ⟨N, hN⟩ := ha (ε / 2) (half_pos hε)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  use N
  -- ⊢ ∀ n ≥ N, |b n - 2 * L| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |b n - 2 * L| < ε
  rw [hb]
  -- ⊢ |2 * a n - 2 * L| < ε
  exact abs_lt.mpr ⟨by linarith [abs_lt.mp (hN n hn)],
                    by linarith [abs_lt.mp (hN n hn)]⟩

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain ⟨N, hN⟩ := ha (ε / 2) (half_pos hε)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  refine ⟨N, fun n hn => ?_⟩
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |b n - 2 * L| < ε
  rw [hb,
      show 2 * a n - 2 * L = 2 * (a n - L) from by ring,
      abs_mul,
      abs_of_pos zero_lt_two]
  -- ⊢ 2 * |a n - L| < ε
  linarith [hN n hn]

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

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain ⟨N, hN⟩ := ha (ε / 2) (half_pos hε)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  exact ⟨N, fun n hn => calc
    |b n - 2 * L|
      = 2 * |a n - L| := by
          rw [hb,
             show 2 * a n - 2 * L = 2 * (a n - L) from by ring,
             abs_mul,
             abs_of_pos zero_lt_two]
    _ < 2 * (ε / 2) := by linarith [hN n hn]
    _ = ε := mul_div_cancel₀ ε two_ne_zero⟩

-- 6ª demostración
-- ===============

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain  ⟨N, hN⟩ := ha (ε / 2) (half_pos hε)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  use N
  -- ⊢ ∀ n ≥ N, |b n - 2 * L| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |b n - 2 * L| < ε
  calc |b n - 2 * L|
       = |2 * a n - 2 * L| := by rw [hb n]
     _ = |2 * (a n - L)|   := by simp only [mul_sub]
     _ = |2| * |a n - L|   := by simp only [abs_mul]
     _ = 2 * |a n - L|     := by simp only [abs_two]
     _ < 2 * (ε / 2)       := by simp only [mul_lt_mul_of_pos_left, hN n hn, two_pos]
     _ = ε                 := by rw [mul_div_cancel₀ ε two_ne_zero]

-- 7ª demostración
-- ===============

example
  (ha : LimSuc a L)
  (hb : ∀ n, b n = 2 * a n)
  : LimSuc b (2 * L) :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |b n - 2 * L| < ε
  obtain  ⟨N, hN⟩ := ha (ε / 2) (half_pos hε)
  -- N : ℕ
  -- hN : ∀ n ≥ N, |a n - L| < ε / 2
  use N
  -- ⊢ ∀ n ≥ N, |b n - 2 * L| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ N
  -- ⊢ |b n - 2 * L| < ε
  calc |b n - 2 * L|
       = |2 * a n - 2 * L| := congr_arg (|· - 2 * L|) (hb n)
     _ = |2 * (a n - L)|   := congr_arg abs (mul_sub 2 (a n) L).symm
     _ = |2| * |a n - L|   := abs_mul 2 (a n - L)
     _ = 2 * |a n - L|     := congr_arg (· * |a n - L|) abs_two
     _ < 2 * (ε / 2)       := mul_lt_mul_of_pos_left (hN n hn) two_pos
     _ = ε                 := mul_div_cancel₀ ε two_ne_zero

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

variable (x y z : ℝ)

#check (abs_lt :|x| < y ↔ -y < x ∧ x < y)
#check (abs_mul x y : |x * y| = |x| * |y|)
#check (abs_of_pos : 0 < x → |x| = x)
#check (abs_two : |(2 : ℝ)| = 2)
#check (half_pos : 0 < x → 0 < x / 2)
#check (mul_div_cancel₀ x : y ≠ 0 → y * (x / y) = x)
#check (mul_lt_mul_of_pos_left : x < y → 0 < z → z * x < z * y)
#check (mul_sub x y z : x * (y - z) = x * y - x * z)
#check (two_ne_zero : 2 ≠ 0)
#check (zero_lt_two : 0 < 2)

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