Menu Close

Día: 5 enero, 2021

ForMatUS: Pruebas en Lean de la unicidad del límite de las sucesiones

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la unicidad del límite de las sucesiones.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
 
variables (u :   )
variables (a b x y : )
 
-- ----------------------------------------------------
-- Nota. Se usarán las siguientes notaciones,
-- definiciones y lemas estudiados anteriormente:
-- + |x| = abs x
-- + limite u c :
--      ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε
-- + cero_de_abs_mn_todos:
--      (∀ ε > 0, |x| ≤ ε) → x = 0
-- + ig_de_abs_sub_mne_todos:
--      (∀ ε > 0, |x - y| ≤ ε) → x = y
-- ----------------------------------------------------
 
notation `|`x`|` := abs x
 
def limite : (  )    Prop :=
λ u c,  ε > 0,  N,  n  N, |u n - c|  ε
 
lemma cero_de_abs_mn_todos
  (h :  ε > 0, |x|  ε)
  : x = 0 :=
abs_eq_zero.mp
  (eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)
 
lemma ig_de_abs_sub_mne_todos
  (h :  ε > 0, |x - y|  ε)
  : x = y :=
sub_eq_zero.mp (cero_de_abs_mn_todos (x - y) h)
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que cada sucesión tiene como
-- máximo un límite.
-- ----------------------------------------------------
 
-- 1ª demostración
example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
begin
  apply ig_de_abs_sub_mne_todos,
  intros ε hε,
  cases ha (ε/2) (half_pos hε) with Na hNa,
  cases hb (ε/2) (half_pos hε) with Nb hNb,
  let N := max Na Nb,
  clear ha hb,
  specialize hNa N (le_max_left  _ _),
  specialize hNb N (le_max_right  _ _),
  calc |a - b|
       = |(a - u N) + (u N - b)| : by ring
   ...  |a - u N| + |u N - b|   : by apply abs_add
   ... = |u N - a| + |u N - b|   : by rw abs_sub
   ...  ε/2 + ε/2               : add_le_add hNa hNb
   ... = ε                       : add_halves ε
end
 
-- 2ª demostración
example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
begin
  apply ig_de_abs_sub_mne_todos,
  intros ε hε,
  cases ha (ε/2) (by linarith) with Na hNa,
  cases hb (ε/2) (by linarith) with Nb hNb,
  let N := max Na Nb,
  clear ha hb,
  specialize hNa N (by finish),
  specialize hNb N (by finish),
  calc |a - b|
       = |(a - u N) + (u N - b)| : by ring
   ...  |a - u N| + |u N - b|   : by apply abs_add
   ... = |u N - a| + |u N - b|   : by rw abs_sub
   ...  ε                       : by linarith [hNa, hNb]
end

Pruebas en Lean de “Si |x – y| ≤ ε, para todo ε > 0, entonces x = y”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad:

Si |x – y| ≤ ε, para todo ε > 0, entonces x = y

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
 
variables (x y : )
 
-- ----------------------------------------------------
-- Ejercicio 1. Definir la notación |x| para el valor
-- absoluto de x.
-- ----------------------------------------------------
 
notation `|`x`|` := abs x
 
-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que si |x - y| ≤ ε, para todo
-- ε > 0, entonces x = y.
-- ----------------------------------------------------
 
-- Se usará el lema demostrado anteriormente
lemma cero_de_abs_mne_todos
  (h :  ε > 0, |x|  ε)
  : x = 0 :=
abs_eq_zero.mp
  (eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)
 
-- 1ª demostración
example
  (h :  ε > 0, |x - y|  ε)
  : x = y :=
begin
  rw ← sub_eq_zero,
  exact cero_de_abs_mne_todos (x - y) h,
end
 
-- 2ª demostración
lemma ig_de_abs_sub_mne_todos
  (h :  ε > 0, |x - y|  ε)
  : x = y :=
sub_eq_zero.mp (cero_de_abs_mne_todos (x - y) h)