Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 3 pruebas en Lean de la propiedad
Toda sucesión convergente es una sucesión de Cauchy
usando los estilos aplicativo y declarativo.
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 |
import data.real.basic variable {u : ℕ → ℝ} -- ---------------------------------------------------- -- Nota. Usaremos los siguientes conceptos estudiados -- anteriormente. -- ---------------------------------------------------- notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε -- ---------------------------------------------------- -- Ejercicio 1. Definir la función -- sucesion_convergente : (ℕ → ℝ) → Prop -- tal que (sucesion_convergente u) expresa que la -- sucesión u es convergente. -- ---------------------------------------------------- def sucesion_convergente : (ℕ → ℝ) → Prop | u := ∃ a, limite u a -- ---------------------------------------------------- -- Ejercicio 2. Definir la función -- sucesion_de_Cauchy : (ℕ → ℝ) → Prop -- tal que (sucesion_de_Cauchy u) expresa que la -- sucesión u es una sucesión de Cauchy. -- ---------------------------------------------------- def sucesion_de_Cauchy : (ℕ → ℝ) → Prop | u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε -- ---------------------------------------------------- -- Ejercicio 3. Demostrar que toda sucesión convergente -- es una sucesión de Cauchy. -- ---------------------------------------------------- -- 1ª demostración example (h : sucesion_convergente u) : sucesion_de_Cauchy u := begin -- unfold sucesion_convergente at h, cases h with a ha, -- unfold sucesion_de_Cauchy, intros ε hε, -- unfold limite at ha, cases ha (ε/2) (half_pos hε) with N hN, use N, intros p q hp hq, calc |u p - u q| = |(u p - a) + (a - u q)| : by ring ... ≤ |u p - a| + |a - u q| : by apply abs_add ... = |u p - a| + |u q - a| : by rw abs_sub (u q) a ... ≤ ε/2 + |u q - a| : add_le_add_right (hN p hp) _ ... ≤ ε/2 + ε/2 : add_le_add_left (hN q hq) (ε/2) ... = ε : add_halves ε end -- 2ª demostración example (h : sucesion_convergente u) : sucesion_de_Cauchy u := begin cases h with a ha, intros ε hε, cases ha (ε/2) (by linarith) with N hN, use N, intros p q hp hq, calc |u p - u q| = |(u p - a) + (a - u q)| : by ring ... ≤ |u p - a| + |a - u q| : by simp only [abs_add] ... = |u p - a| + |u q - a| : by simp only [abs_add, abs_sub] ... ≤ ε : by linarith [hN p hp, hN q hq], end -- 3ª demostración example (h : sucesion_convergente u) : sucesion_de_Cauchy u := exists.elim h (assume a, assume ha : limite u a, show sucesion_de_Cauchy u, from (assume ε, assume hε : ε > 0, exists.elim (ha (ε/2) (by linarith)) (assume N, assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε/2, show ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε, from exists.intro N (assume p q, assume hp: p ≥ N, assume hq: q ≥ N, show |u p - u q| ≤ ε, from calc |u p - u q| = |(u p - a) + (a - u q)| : by ring ... ≤ |u p - a| + |a - u q| : by simp only [abs_add] ... = |u p - a| + |u q - a| : by simp only [abs_add, abs_sub] ... ≤ ε : by linarith [hN p hp, hN q hq])))) |