ForMatUS: Pruebas en Lean de “El punto de acumulación de las convergentes es su límite”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad
Si a es un punto de acumulación de una sucesión convergente u, entonces a es el límite de u.
usando los estilos declarativo, aplicativos y funcional.
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 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 |
import data.real.basic variable {u : ℕ → ℝ} variables {a b: ℝ} variables (x y : ℝ) variable {φ : ℕ → ℕ} -- ---------------------------------------------------- -- Nota. Usaremos los siguientes conceptos estudiados -- anteriormente. -- ---------------------------------------------------- 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) lemma unicidad_limite (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, 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 def extraccion : (ℕ → ℕ) → Prop | φ := ∀ n m, n < m → φ n < φ m lemma id_mne_extraccion (h : extraccion φ) : ∀ n, n ≤ φ n := begin intros n, induction n with m HI, { linarith }, { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) }, end def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop | u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a lemma limite_subsucesion (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := assume ε, assume hε : ε > 0, exists.elim (h ε hε) ( assume N, assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε, have h1 : ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε, { assume n, assume hn : n ≥ N, have h2 : N ≤ φ n, from calc N ≤ n : hn ... ≤ φ n : id_mne_extraccion hφ n, show |(u ∘ φ) n - a| ≤ ε, from hN (φ n) h2, }, show ∃ N, ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε, from exists.intro N h1) -- ---------------------------------------------------- -- Ejercicio. Demostrar que si a es un punto de -- acumulación de una sucesión de límite b, entonces a -- y b son iguales. -- ---------------------------------------------------- -- 1ª demostración example (ha : punto_acumulacion u a) (hb : limite u b) : a = b := begin -- unfold punto_acumulacion at ha, rcases ha with ⟨φ, hφ₁, hφ₂⟩, have hφ₃ : limite (u ∘ φ) b, from limite_subsucesion hb hφ₁, exact unicidad_limite hφ₂ hφ₃, end -- 2ª demostración example (ha : punto_acumulacion u a) (hb : limite u b) : a = b := begin rcases ha with ⟨φ, hφ₁, hφ₂⟩, exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁), end -- 3ª demostración example (ha : punto_acumulacion u a) (hb : limite u b) : a = b := exists.elim ha (λ φ hφ, unicidad_limite hφ.2 (limite_subsucesion hb hφ.1)) -- 4ª demostración example (ha : punto_acumulacion u a) (hb : limite u b) : a = b := exists.elim ha ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, have hφ' : limite (u ∘ φ) b, from limite_subsucesion hb hφ.1, show a = b, from unicidad_limite hφ.2 hφ') |