ForMatUS: Pruebas en Lean del teorema del emparedado
He añadido a la lista Lógica con Lean el vídeo Teorema del emparedado en el que se comentan pruebas en Lean del teorema del emparedado:
Si dos sucesiones tienen el mismo límite, entonces las sucesiones que están comprendidas entre éstas también tienen el mismo límite.
A continuación, se muestra el vídeo
|
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 134 135 136 137 138 139 140 141 142 143 144 145 146 147 |
import data.real.basic variables (u v w : ℕ → ℝ) variable (a : ℝ) -- ---------------------------------------------------- -- Ejercicio 1. Definir la notación |x| para el valor -- absoluto de x. -- ---------------------------------------------------- notation `|`x`|` := abs x -- ---------------------------------------------------- -- Ejercicio 2. Definir la función -- limite : (ℕ → ℝ) → ℝ → Prop -- tal que (limite u c) expresa que c es el límite de -- la sucesión u. -- ---------------------------------------------------- def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε -- ---------------------------------------------------- -- Ejercicio 3. Demostrar que si dos sucesiones tienen -- el mismo límite, entonces las sucesiones que están -- comprendidas entre éstas también tienen el mismo -- límite. -- ---------------------------------------------------- -- Nota. En la demostración se usará el siguiente lema: lemma max_ge_iff {p q r : ℕ} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff -- 1ª demostración -- =============== example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := begin intros ε hε, cases hu ε hε with N hN, clear hu, cases hw ε hε with N' hN', clear hw hε, use max N N', intros n hn, rw max_ge_iff at hn, specialize hN n hn.1, specialize hN' n hn.2, specialize h n, specialize h' n, clear hn, rw abs_le at *, split, { calc -ε ≤ u n - a : hN.1 ... ≤ v n - a : by linarith, }, { calc v n - a ≤ w n - a : by linarith ... ≤ ε : hN'.2, }, end -- 2ª demostración example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := begin intros ε hε, cases hu ε hε with N hN, clear hu, cases hw ε hε with N' hN', clear hw hε, use max N N', intros n hn, rw max_ge_iff at hn, specialize hN n (by linarith), specialize hN' n (by linarith), specialize h n, specialize h' n, rw abs_le at *, split, { linarith, }, { linarith, }, end -- 3ª demostración example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := begin intros ε hε, cases hu ε hε with N hN, clear hu, cases hw ε hε with N' hN', clear hw hε, use max N N', intros n hn, rw max_ge_iff at hn, specialize hN n (by linarith), specialize hN' n (by linarith), specialize h n, specialize h' n, rw abs_le at *, split ; linarith, end -- 4ª demostración example (hu : limite u a) (hw : limite w a) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : limite v a := assume ε, assume hε : ε > 0, exists.elim (hu ε hε) ( assume N, assume hN : ∀ (n : ℕ), n ≥ N → |u n - a| ≤ ε, exists.elim (hw ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |w n - a| ≤ ε, show ∃ N, ∀ n, n ≥ N → |v n - a| ≤ ε, from exists.intro (max N N') ( assume n, assume hn : n ≥ max N N', have h1 : n ≥ N ∧ n ≥ N', from max_ge_iff.mp hn, have h2 : -ε ≤ v n - a, { have h2a : |u n - a| ≤ ε, from hN n h1.1, calc -ε ≤ u n - a : and.left (abs_le.mp h2a) ... ≤ v n - a : by linarith [h n], }, have h3 : v n - a ≤ ε, { have h3a : |w n - a| ≤ ε, from hN' n h1.2, calc v n - a ≤ w n - a : by linarith [h' n] ... ≤ ε : and.right (abs_le.mp h3a), }, show |v n - a| ≤ ε, from abs_le.mpr (and.intro h2 h3)))) |