Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b
Demostrar con Lean4 que si la sucesión \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Real.Basic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by sorry |
1. Demostración en lenguaje natural
En la demostración usaremos los siguientes lemas
\begin{align}
&(∀ a ∈ ℝ)\left[a > 0 → \frac{a}{2} > 0\right] \tag{L1} \\
&(∀ a, b, c ∈ ℝ)[\max(a, b) ≤ c → a ≤ c] \tag{L2} \\
&(∀ a, b, c ∈ ℝ)[\max(a, b) ≤ c → b ≤ c] \tag{L3} \\
&(∀ a, b ∈ ℝ)[|a + b| ≤ |a| + |b|] \tag{L4} \\
&(∀ a ∈ ℝ)\left[\frac{a}{2} + \frac{a}{2} = a\right] \tag{L5}
\end{align}
Tenemos que probar que para todo \(ε ∈ ℝ\), si
\[ ε > 0 \tag{1} \]
entonces
\[ (∃N ∈ ℕ)(∀n ∈ ℕ)[n ≥ N → |(u + v)(n) – (a + b)| < ε] \tag{2} \]
Por (1) y el lema L1, se tiene que
\[ \frac{ε}{2} > 0 \tag{3} \]
Por (3) y porque el límite de \(u\) es \(a\), se tiene que
\[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |u(n) – a| < \frac{ε}{2}\right] \]
Sea \(N₁ ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ N₁ → |u(n) – a| < \frac{ε}{2}\right] \tag{4} \]
Por (3) y porque el límite de \(v\) es \(b\), se tiene que
\[ (∃N ∈ ℕ)(∀n ∈ ℕ)\left[n ≥ N → |v(n) – b| < \frac{ε}{2}\right] \]
Sea \(N₂ ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ N₂ → |v(n) – b| < \frac{ε}{2}\right] \tag{5} \]
Sea \(N = \max(N₁, N₂)\). Veamos que verifica la condición (1). Para ello, sea \(n ∈ ℕ\) tal que \(n ≥ N\). Entonces, \(n ≥ N₁\) (por L2) y \(n ≥ N₂\) (por L3). Por tanto, usando las propiedades (4) y (5) se tiene que
\begin{align}
|u(n) – a| &< \frac{ε}{2} \tag{6} \\
|v(n) – b| &< \frac{ε}{2} \tag{7}
\end{align}
Finalmente,
\begin{align}
|(u + v)(n) – (a + b)| &= |(u(n) + v(n)) – (a + b)| \\
&= |(u(n) – a) + (v(n) – b)| \\
&≤ |u(n) – a| + |v(n) – b| &&\text{[por L4]}\\
&< \frac{ε}{2} + \frac{ε}{2} &&\text{[por (6) y (7)]}\\
&= ε &&\text{[por L5]}
\end{align}
2. Demostraciones con Lean4
|
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 165 166 167 168 169 170 171 172 173 174 175 176 177 178 |
import Mathlib.Data.Real.Basic variable {s t : ℕ → ℝ} {a b c : ℝ} def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε -- 1ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u + v) n - (a + b)| < ε have hε2 : 0 < ε / 2 := half_pos hε cases' hu (ε / 2) hε2 with Nu hNu -- Nu : ℕ -- hNu : ∀ (n : ℕ), n ≥ Nu → |u n - a| < ε / 2 cases' hv (ε / 2) hε2 with Nv hNv -- Nv : ℕ -- hNv : ∀ (n : ℕ), n ≥ Nv → |v n - b| < ε / 2 clear hu hv hε2 hε let N := max Nu Nv use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(s + t) n - (a + b)| < ε intros n hn -- n : ℕ -- hn : n ≥ N have nNu : n ≥ Nu := le_of_max_le_left hn specialize hNu n nNu -- hNu : |u n - a| < ε / 2 have nNv : n ≥ Nv := le_of_max_le_right hn specialize hNv n nNv -- hNv : |v n - b| < ε / 2 clear hn nNu nNv calc |(u + v) n - (a + b)| = |(u n + v n) - (a + b)| := rfl _ = |(u n - a) + (v n - b)| := by { congr; ring } _ ≤ |u n - a| + |v n - b| := by apply abs_add _ < ε / 2 + ε / 2 := by linarith [hNu, hNv] _ = ε := by apply add_halves -- 2ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by 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 rfl _ = |(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 -- 3ª demostración -- =============== lemma max_ge_iff {α : Type _} [LinearOrder α] {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) := by 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 -- 4ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by 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 rfl _ = |(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 -- 5ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by 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 rfl _ = |(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)] -- 6ª demostración -- =============== example (hu : limite u a) (hv : limite v b) : limite (u + v) (a + b) := by 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 rfl _ = |(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 -- Lemas usados -- ============ -- variable (d : ℝ) -- #check (abs_add a b : |a + b| ≤ |a| + |b|) -- #check (add_halves a : a / 2 + a / 2 = a) -- #check (add_lt_add : a < b → c < d → a + c < b + d) -- #check (half_pos : a > 0 → a / 2 > 0) -- #check (le_max_left a b : a ≤ max a b) -- #check (le_max_right a b : b ≤ max a b) -- #check (le_of_max_le_left : max a b ≤ c → a ≤ c) -- #check (le_of_max_le_right : max a b ≤ c → b ≤ c) -- #check (max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones 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 |
theory Limite_de_sucesiones_constantes 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 "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" proof (intro allI impI) fix n :: nat assume "0 ≤ n" have "c - c = 0" by (simp only: diff_self) then have "¦c - c¦ = 0" by (simp only: abs_eq_0_iff) also have "… < ε" by (simp only: ‹0 < ε›) finally show "¦c - c¦ < ε" by this qed then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 2ª demostración *) lemma "limite (λ n. c) c" proof (unfold limite_def) show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" have "∀n≥0::nat. ¦c - c¦ < ε" by (simp add: ‹0 < ε›) then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI) qed qed (* 3ª demostración *) lemma "limite (λ n. c) c" unfolding limite_def by simp (* 4ª demostración *) lemma "limite (λ n. c) c" by (simp add: limite_def) end |
