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
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 |
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 |