Límite de la suma de sucesiones convergentes
En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.
Se define que a es el límite de la sucesión u, por
1 2 |
def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε |
donde se usa la notación |x| para el valor absoluto de x
1 |
notation `|`x`|` := abs x |
Demostrar que el límite de la suma de dos sucesiones convergentes es la suma de los límites de dichas sucesiones.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import data.real.basic variables (u v : ℕ → ℝ) variables (a b : ℝ) notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := sorry |
[expand title=»Soluciones con Lean»]
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 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 |
import data.real.basic variables (u v : ℕ → ℝ) variables (a b : ℝ) notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := begin intros ε hε, have hε2 : 0 < ε / 2, { linarith }, cases hu (ε / 2) hε2 with Nu hNu, cases hv (ε / 2) hε2 with Nv hNv, clear hu hv hε2 hε, use max Nu Nv, intros n hn, have hn₁ : n ≥ Nu, { exact le_of_max_le_left hn }, specialize hNu n hn₁, have hn₂ : n ≥ Nv, { exact le_of_max_le_right hn }, specialize hNv n hn₂, clear hn hn₁ hn₂ Nu Nv, calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| : by refl ... = |(u n - a) + (v n - b)| : by {congr, ring} ... ≤ |u n - a| + |v n - b| : by apply abs_add ... < ε / 2 + ε / 2 : by linarith ... = ε : by apply add_halves, end -- 2ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := begin intros ε hε, cases hu (ε/2) (by linarith) with Nu hNu, cases hv (ε/2) (by linarith) with Nv hNv, use max Nu Nv, intros n hn, have hn₁ : n ≥ Nu := le_of_max_le_left hn, specialize hNu n hn₁, have hn₂ : n ≥ Nv := le_of_max_le_right hn, specialize hNv n hn₂, calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| : by refl ... = |(u n - a) + (v n - b)| : by {congr, ring} ... ≤ |u n - a| + |v n - b| : by apply abs_add ... < ε / 2 + ε / 2 : by linarith ... = ε : by apply add_halves, end -- 3ª demostración -- =============== lemma max_ge_iff {α : Type*} [linear_order α] {p q r : α} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := max_le_iff example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := begin intros ε hε, cases hu (ε/2) (by linarith) with Nu hNu, cases hv (ε/2) (by linarith) with Nv hNv, use max Nu Nv, intros n hn, cases max_ge_iff.mp hn with hn₁ hn₂, have cota₁ : |u n - a| < ε/2 := hNu n hn₁, have cota₂ : |v n - b| < ε/2 := hNv n hn₂, calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| : by rfl ... = |(u n - a) + (v n - b)| : by { congr, ring } ... ≤ |u n - a| + |v n - b| : by apply abs_add ... < ε : by linarith, end -- 4ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := begin intros ε hε, cases hu (ε/2) (by linarith) with Nu hNu, cases hv (ε/2) (by linarith) with Nv hNv, use max Nu Nv, intros n hn, cases max_ge_iff.mp hn with hn₁ hn₂, calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| : by refl ... = |(u n - a) + (v n - b)| : by { congr, ring } ... ≤ |u n - a| + |v n - b| : by apply abs_add ... < ε/2 + ε/2 : add_lt_add (hNu n hn₁) (hNv n hn₂) ... = ε : by simp end -- 5ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := begin intros ε hε, cases hu (ε/2) (by linarith) with Nu hNu, cases hv (ε/2) (by linarith) with Nv hNv, use max Nu Nv, intros n hn, rw max_ge_iff at hn, calc |(u + v) n - (a + b)| = |u n + v n - (a + b)| : by refl ... = |(u n - a) + (v n - b)| : by { congr, ring } ... ≤ |u n - a| + |v n - b| : by apply abs_add ... < ε : by linarith [hNu n (by linarith), hNv n (by linarith)], end -- 6ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := begin intros ε Hε, cases hu (ε/2) (by linarith) with L HL, cases hv (ε/2) (by linarith) with M HM, set N := max L M with hN, use N, have HLN : N ≥ L := le_max_left _ _, have HMN : N ≥ M := le_max_right _ _, intros n Hn, have H3 : |u n - a| < ε/2 := HL n (by linarith), have H4 : |v n - b| < ε/2 := HM n (by linarith), calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| : by refl ... = |(u n - a) + (v n - b)| : by { congr, ring } ... ≤ |(u n - a)| + |(v n - b)| : by apply abs_add ... < ε/2 + ε/2 : by linarith ... = ε : by ring end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
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 |
theory Limite_de_la_suma_de_sucesiones_convergentes imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" (* 1ª demostración *) lemma assumes "limite u a" "limite v b" shows "limite (λ n. u n + v n) (a + b)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp then have "∃k. ∀n≥k. ¦u n - a¦ < ε/2" using assms(1) limite_def by blast then obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2" by (rule exE) then have "∃k. ∀n≥k. ¦v n - b¦ < ε/2" using ‹0 < ε/2› assms(2) limite_def by blast then obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2" by (rule exE) have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε" proof (intro allI impI) fix n :: nat assume "n ≥ max Nu Nv" have "¦(u n + v n) - (a + b)¦ = ¦(u n - a) + (v n - b)¦" by simp also have "… ≤ ¦u n - a¦ + ¦v n - b¦" by simp also have "… < ε/2 + ε/2" using hNu hNv ‹max Nu Nv ≤ n› by fastforce finally show "¦(u n + v n) - (a + b)¦ < ε" by simp qed then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε " by (rule exI) qed qed (* 2ª demostración *) lemma assumes "limite u a" "limite v b" shows "limite (λ n. u n + v n) (a + b)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2" using ‹0 < ε/2› assms(1) limite_def by blast obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2" using ‹0 < ε/2› assms(2) limite_def by blast have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε" using hNu hNv by (smt (verit, ccfv_threshold) field_sum_of_halves max.boundedE) then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε " by blast qed qed end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]