Ir al contenido principal

Reto 2: La sucesión 1, -1, 1, -1,... no es convergente

También disponible en:

English

Demostrar que la sucesión definida por 1, -1, 1, -1,... no converge.

Para ello, se propone completar la siguiente demostración en Lean 4:

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

variable {a : ℕ → ℝ}

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

def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SeqConv a :=
by sorry

1. Demostración en lenguaje natural

Sea \(a\) la sucesión definida por \(a(n) = (-1)^n\). Supongamos que \(a\) es convergente. Entonces, existe un \(L\) tal que \(a\) converge a \(L\). Por tanto, existe un \(k ∈ ℕ\) tal que, \[ ∀n ≥ k, |a(n) - L| < 1/2 \tag{1} \] Entonces, \begin{align} 2 &= |2| \newline &= |(1 - L) + (1 + L)| \newline &= |(1 - L) + (-1)(-1 - L)| \newline &≤ |1 - L| + |(-1)(-1 - L)| \newline &= |1 - L| + |-1 - L| \newline &= |(-1)^{2k} - L| + |(-1)^{2k+1} - L| \newline &= |a(2k) - L| + |a(2k+1) - L| \newline &< 1/2 + 1/2 &\text{[por (1), \(2k ≥ k\) y \(2k+1 ≥ k\)]} \newline &= 1 \newline \end{align} Luego, 2 < 1 que es una contradicción.

2. Demostraciones con Lean4

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

variable {a : ℕ → ℝ}

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

def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

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

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SeqConv a :=
by
  intro h
  -- h : SeqConv a
  -- ⊢ False
  obtain ⟨L, hL⟩ := h
  -- L : ℝ
  -- hL : SeqLim a L
  obtain ⟨k, hk⟩ := hL (1/2) (by grind)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < 1 / 2
  have h1 : ¬(2 : ℝ) < 1 := lt_asymm one_lt_two
  apply h1
  -- ⊢ 2 < 1
  calc
    2 = |2|                                        := by grind
    _ = |(1 - L) + (1 + L)|                        := by grind
    _ = |(1 - L) + (-1)*(-1 - L)|                  := by grind
    _ ≤ |1 - L| + |(-1)*(-1 - L)|                  := by grind
    _ = |1 - L| + |-1 - L|                         := by grind
    _ = |(-1:ℝ)^(2*k) - L| + |(-1:ℝ)^(2*k+1) - L|  := by
          have h2 : (-1:ℝ)^(2*k) = 1    := by simp
          have h3 : (-1:ℝ)^(2*k+1) = -1 := by grind
          rw [h2, h3]
    _ = |a (2*k) - L| + |a (2*k+1) - L|            := by simp [*]
    _ < 1/2 + 1/2                                  := by grind
    _ = 1                                          := by grind

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

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬SeqConv a :=
by
  rintro ⟨L, hL⟩
  -- L : ℝ
  -- hL : SeqLim a L
  -- ⊢ False
  obtain ⟨k, hk⟩ := hL (1 / 2) (by positivity)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < 1 / 2
  have h1 := hk (2 * k) (by omega)
  -- h1 : |a (2 * k) - L| < 1 / 2
  have h2 := hk (2 * k + 1) (by omega)
  -- h2 : |a (2 * k + 1) - L| < 1 / 2
  simp only [ha, pow_succ] at h1 h2
  -- h1 : |(-1) ^ (2 * k) - L| < 1 / 2
  -- h2 : |(-1) ^ (2 * k) * -1 - L| < 1 / 2
  norm_num at h1 h2
  -- h1 : |1 - L| < 1 / 2
  -- h2 : |-1 - L| < 1 / 2
  rw [abs_lt] at h1 h2
  -- h1 : -(1 / 2) < 1 - L ∧ 1 - L < 1 / 2
  -- h2 : -(1 / 2) < -1 - L ∧ -1 - L < 1 / 2
  linarith

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

variable {x y z x' y' : ℝ}
variable {m n k : ℕ}
variable (f : ℝ → ℝ)

lemma L1 : (1 - x) + (1 + x) = 2 := by
  calc (1 - x) + (1 + x)
       = 1 + 1             := sub_add_add_cancel 1 1 x
     _ = 2                 := one_add_one_eq_two

lemma L2 : (-1:ℝ) * -1 = 1 := by
  calc (-1:ℝ) * -1
       = 1 * 1   := neg_mul_neg 1 1
     _ = 1       := one_mul 1

lemma L3 : -1 * -x = x := by
  calc -1 * -x
       = -(1 * -x) := neg_mul 1 (-x)
     _ = - -x      := congr_arg (- ·) (one_mul (-x))
     _ = x         := neg_neg x

lemma L4 : -1 * (-1 - x) = 1 + x := by
  calc -1 * (-1 - x)
       = -1 * (-1 + -x)     := congr_arg (-1 * ·) (sub_eq_add_neg (-1) x)
     _ = -1 * -1 + -1 * -x  := left_distrib (-1) (-1) (-x)
     _ = 1 + -1 * -x        := congr_arg (· + (-1)*(-x)) L2
     _ = 1 + x              := congr_arg ( 1 + ·) L3

lemma L5 : |-1 * (-1 - x)| = |-1 - x| := by
  calc |-1 * (-1 - x)|
       = |-1| * |-1 - x| := abs_mul (-1) (-1 - x)
     _ = |1| * |-1 - x|  := congrArg (· * |-1 - x|) (abs_neg 1)
     _ = 1 * |-1 - x|    := congrArg (· * |-1 - x|) abs_one
     _ = |-1 - x|        := one_mul |-1 - x|

lemma L6 : (-1:ℝ)^(2*n) = 1 := by
  calc (-1:ℝ)^(2*n)
       = ((-1:ℝ)^2)^n := pow_mul (-1) 2 n
     _ = (1:ℝ)^n      := congr_arg ( · ^ n) neg_one_sq
     _ = 1            := one_pow n

lemma L7 : (-1:ℝ)^(2*n+1) = -1 := by
  calc (-1:ℝ)^(2*n+1)
       = (-1)^(2*n) * -1 := pow_succ (-1) (2 * n)
     _ = 1 * -1          := congr_arg (· * -1) L6
     _ = -1              := one_mul (-1)

lemma L8 : n ≤ 2 * n := by
  calc n
       = 1 * n := (one_mul n).symm
     _ ≤ 2 * n := Nat.mul_le_mul_right n one_le_two

lemma L9
  (hk : ∀ n ≥ k, |a n - x| < 1 / 2)
  : |a (2*k) - x| < 1 / 2 :=
hk (2*k) L8

lemma L10 : n ≤ 2 * n + 1 := by
  calc n
       ≤ 2 * n     := L8
     _ ≤ 2 * n + 1 := Nat.le_add_right (2 * n) 1

lemma L11
  (hk : ∀ n ≥ k, |a n - x| < 1 / 2)
  : |a (2*k+1) - x| < 1 / 2 :=
hk (2*k+1) L10

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SeqConv a :=
by
  intro h
  -- h : SeqConv a
  -- ⊢ False
  obtain ⟨L, hL⟩ := h
  -- L : ℝ
  -- hL : SeqLim a L
  obtain ⟨k, hk⟩ := hL (1/2) one_half_pos
  -- k : ℕ
  -- hk : ∀ n ≥ k, |a n - L| < 1 / 2
  have h1 : ¬(2 : ℝ) < 1 := Nat.not_ofNat_lt_one
  apply h1
  -- ⊢ 2 < 1
  calc
    2 = |2| :=
          abs_two.symm
    _ = |(1 - L) + (1 + L)| :=
          congrArg abs L1.symm
    _ = |(1 - L) + (-1)*(-1 - L)| :=
          congr_arg (abs ((1 - L) + ·)) L4.symm
    _ ≤ |1 - L| + |(-1)*(-1 - L)| :=
          abs_add_le (1 - L) (-1 * (-1 - L))
    _ = |1 - L| + |-1 - L| :=
          congr_arg (|1 - L| + ·) L5
    _ = |(-1:ℝ)^(2*k) - L| + |(-1:ℝ)^(2*k+1) - L|  :=
          congrArg₂ (|· - L| + |· - L|) L6.symm L7.symm
    _ = |a (2*k) - L| + |a (2*k+1) - L| :=
          congrArg₂ (· + ·)
            (congrArg (|· - L|) (ha (2*k)).symm)
            (congrArg (|· - L|) (ha (2*k+1)).symm)
    _ < 1 / 2 + 1 / 2 :=
          add_lt_add (L9 hk) (L11 hk)
    _ = 1 := add_halves 1

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

variable (a b c d : ℝ)
#check (Nat.le_add_right n k : n ≤ n + k)
#check (Nat.mul_le_mul_right k : n ≤ m → n * k ≤ m * k)
#check (abs_add_le a b : |a + b| ≤ |a| + |b|)
#check (abs_lt : |a| < b ↔ -b < a ∧ a < b)
#check (abs_mul a b : |a * b| = |a| * |b|)
#check (abs_neg a : |(-a)| = |a|)
#check (abs_one : |(1 : ℝ)| = 1)
#check (abs_two : |(2 : ℝ)| = 2)
#check (add_halves a : a / 2 + a / 2 = a)
#check (add_lt_add : a < b → c < d → a + c < b + d)
#check (left_distrib a b c : a * (b + c) = a * b + a * c)
#check (lt_asymm  : a < b → ¬b < a)
#check (neg_mul a b : -a * b = -(a * b))
#check (neg_mul_neg a b : -a * -b = a * b)
#check (neg_neg a : - -a = a)
#check (neg_one_sq : (-1) ^ 2 = 1)
#check (one_add_one_eq_two : 1 + 1 = 2)
#check (one_half_pos : (0 : ℝ) < 1 / 2)
#check (one_lt_two : 1 < 2)
#check (one_mul a : 1 * a = a)
#check (one_pow n : 1 ^ n = 1)
#check (pow_mul a m n : a ^ (m * n) = (a ^ m) ^ n)
#check (pow_succ a n : a ^ (n + 1) = a ^ n * a)
#check (sub_add_add_cancel a b c : a - c + (b + c) = a + b)
#check (sub_eq_add_neg a b : a - b = a + -b)

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

3. Soluciones colaborativas

¿Has encontrado una demostración distinta de las publicadas? Puedes compartirla en los comentarios de abajo siguiendo estos pasos:

  • Escribe tu demostración en live.lean-lang.org y comprueba que se compila sin errores.
  • Copia el código y publícalo en los comentarios de esta entrada, dentro de un bloque de código de Lean:
```lean
   -- tu demostración
```

Comentarios