Pruebas en Lean de “Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 2 pruebas en Lean de la propiedad
Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u.
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 : ℕ → ℝ} variables {a : ℝ} variable {φ : ℕ → ℕ} -- ---------------------------------------------------- -- Nota. Usaremos los siguientes conceptos estudiados -- anteriormente. -- ---------------------------------------------------- notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε 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 lemma extraccion_mye (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := λ N N', ⟨max N N', le_max_right N N', le_trans (le_max_left N N') (id_mne_extraccion h (max N N'))⟩ def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop | u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a lemma cerca_acumulacion (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε := begin intros ε hε N, rcases h with ⟨φ, hφ1, hφ2⟩, cases hφ2 ε hε with N' hN', rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩, exact ⟨φ m, hm', hN' _ hm⟩, end def sucesion_de_Cauchy : (ℕ → ℝ) → Prop | u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε -- ---------------------------------------------------- -- Ejercicio. Demostrar que si u es una sucesión de -- Cauchy y a es un punto de acumulación de u, entonces -- a es el límite de u. -- ---------------------------------------------------- -- 1ª demostración example (hu : sucesion_de_Cauchy u) (ha : punto_acumulacion u a) : limite u a := begin -- unfold limite, intros ε hε, -- unfold sucesion_de_Cauchy at hu, cases hu (ε/2) (half_pos hε) with N hN, use N, have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2, apply cerca_acumulacion ha (ε/2) (half_pos hε), cases ha' with N' h, cases h with hNN' hN', intros n hn, calc |u n - a| = |(u n - u N') + (u N' - a)| : by ring ... ≤ |u n - u N'| + |u N' - a| : abs_add (u n - u N') (u N' - a) ... ≤ ε/2 + |u N' - a| : add_le_add_right (hN n N' hn hNN') _ ... ≤ ε/2 + ε/2 : add_le_add_left hN' (ε / 2) ... = ε : add_halves ε end -- 2ª demostración example (hu : sucesion_de_Cauchy u) (ha : punto_acumulacion u a) : limite u a := begin intros ε hε, cases hu (ε/2) (by linarith) with N hN, use N, have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2, apply cerca_acumulacion ha (ε/2) (by linarith), rcases ha' with ⟨N', hNN', hN'⟩, intros n hn, calc |u n - a| = |(u n - u N') + (u N' - a)| : by ring ... ≤ |u n - u N'| + |u N' - a| : by simp [abs_add] ... ≤ ε : by linarith [hN n N' hn hNN'], end |