Demostrar con Lean4 que si la sucesi\u00f3n \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {s t : \u2115 \u2192 \u211d} {a b c : \u211d}\n\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
En la demostraci\u00f3n usaremos los siguientes lemas
\n\begin{align}
\n &(\u2200 a \u2208 \u211d)\left[a > 0 \u2192 \frac{a}{2} > 0\right] \tag{L1} \\
\n &(\u2200 a, b, c \u2208 \u211d)[\max(a, b) \u2264 c \u2192 a \u2264 c] \tag{L2} \\
\n &(\u2200 a, b, c \u2208 \u211d)[\max(a, b) \u2264 c \u2192 b \u2264 c] \tag{L3} \\
\n &(\u2200 a, b \u2208 \u211d)[|a + b| \u2264 |a| + |b|] \tag{L4} \\
\n &(\u2200 a \u2208 \u211d)\left[\frac{a}{2} + \frac{a}{2} = a\right] \tag{L5}
\n\end{align}<\/p>\n
Tenemos que probar que para todo \(\u03b5 \u2208 \u211d\), si
\n\[ \u03b5 > 0 \tag{1} \]
\nentonces
\n\[ (\u2203N \u2208 \u2115)(\u2200n \u2208 \u2115)[n \u2265 N \u2192 |(u + v)(n) - (a + b)| < \u03b5] \tag{2} \]<\/p>\n
Por (1) y el lema L1, se tiene que
\n\[ \frac{\u03b5}{2} > 0 \tag{3} \]
\nPor (3) y porque el l\u00edmite de \(u\) es \(a\), se tiene que
\n\[ (\u2203N \u2208 \u2115)(\u2200n \u2208 \u2115)\left[n \u2265 N \u2192 |u(n) - a| < \frac{\u03b5}{2}\right] \]
\nSea \(N\u2081 \u2208 \u2115\) tal que
\n\[ (\u2200n \u2208 \u2115)\left[n \u2265 N\u2081 \u2192 |u(n) - a| < \frac{\u03b5}{2}\right] \tag{4} \]
\nPor (3) y porque el l\u00edmite de \(v\) es \(b\), se tiene que
\n\[ (\u2203N \u2208 \u2115)(\u2200n \u2208 \u2115)\left[n \u2265 N \u2192 |v(n) - b| < \frac{\u03b5}{2}\right] \]
\nSea \(N\u2082 \u2208 \u2115\) tal que
\n\[ (\u2200n \u2208 \u2115)\left[n \u2265 N\u2082 \u2192 |v(n) - b| < \frac{\u03b5}{2}\right] \tag{5} \]
\nSea \(N = \max(N\u2081, N\u2082)\). Veamos que verifica la condici\u00f3n (1). Para ello, sea \(n \u2208 \u2115\) tal que \(n \u2265 N\). Entonces, \(n \u2265 N\u2081\) (por L2) y \(n \u2265 N\u2082\) (por L3). Por tanto, usando las propiedades (4) y (5) se tiene que
\n\begin{align}
\n |u(n) - a| &< \frac{\u03b5}{2} \tag{6} \\
\n |v(n) - b| &< \frac{\u03b5}{2} \tag{7}
\n\end{align}
\nFinalmente,
\n\begin{align}
\n |(u + v)(n) - (a + b)| &= |(u(n) + v(n)) - (a + b)| \\
\n &= |(u(n) - a) + (v(n) - b)| \\
\n &\u2264 |u(n) - a| + |v(n) - b| &&\text{[por L4]}\\
\n &< \frac{\u03b5}{2} + \frac{\u03b5}{2} &&\text{[por (6) y (7)]}\\
\n &= \u03b5 &&\text{[por L5]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\nvariable {s t : \u2115 \u2192 \u211d} {a b c : \u211d}\n\ndef limite (s : \u2115 \u2192 \u211d) (a : \u211d) :=\n \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |s n - a| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby\n intros \u03b5 h\u03b5\n -- \u03b5 : \u211d\n -- h\u03b5 : \u03b5 > 0\n -- \u22a2 \u2203 N, \u2200 (n : \u2115), n \u2265 N \u2192 |(u + v) n - (a + b)| < \u03b5\n have h\u03b52 : 0 < \u03b5 \/ 2 := half_pos h\u03b5\n cases' hu (\u03b5 \/ 2) h\u03b52 with Nu hNu\n -- Nu : \u2115\n -- hNu : \u2200 (n : \u2115), n \u2265 Nu \u2192 |u n - a| < \u03b5 \/ 2\n cases' hv (\u03b5 \/ 2) h\u03b52 with Nv hNv\n -- Nv : \u2115\n -- hNv : \u2200 (n : \u2115), n \u2265 Nv \u2192 |v n - b| < \u03b5 \/ 2\n clear hu hv h\u03b52 h\u03b5\n let N := max Nu Nv\n use N\n -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(s + t) n - (a + b)| < \u03b5\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 N\n have nNu : n \u2265 Nu := le_of_max_le_left hn\n specialize hNu n nNu\n -- hNu : |u n - a| < \u03b5 \/ 2\n have nNv : n \u2265 Nv := le_of_max_le_right hn\n specialize hNv n nNv\n -- hNv : |v n - b| < \u03b5 \/ 2\n clear hn nNu nNv\n calc |(u + v) n - (a + b)|\n = |(u n + v n) - (a + b)| := rfl\n _ = |(u n - a) + (v n - b)| := by { congr; ring }\n _ \u2264 |u n - a| + |v n - b| := by apply abs_add\n _ < \u03b5 \/ 2 + \u03b5 \/ 2 := by linarith [hNu, hNv]\n _ = \u03b5 := by apply add_halves\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby\n intros \u03b5 h\u03b5\n cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n use max Nu Nv\n intros n hn\n have hn\u2081 : n \u2265 Nu := le_of_max_le_left hn\n specialize hNu n hn\u2081\n have hn\u2082 : n \u2265 Nv := le_of_max_le_right hn\n specialize hNv n hn\u2082\n calc |(u + v) n - (a + b)|\n = |(u n + v n) - (a + b)| := by rfl\n _ = |(u n - a) + (v n - b)| := by {congr; ring}\n _ \u2264 |u n - a| + |v n - b| := by apply abs_add\n _ < \u03b5 \/ 2 + \u03b5 \/ 2 := by linarith\n _ = \u03b5 := by apply add_halves\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nlemma max_ge_iff\n {\u03b1 : Type _}\n [LinearOrder \u03b1]\n {p q r : \u03b1}\n : r \u2265 max p q \u2194 r \u2265 p \u2227 r \u2265 q :=\nmax_le_iff\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby\n intros \u03b5 h\u03b5\n cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n use max Nu Nv\n intros n hn\n cases' max_ge_iff.mp hn with hn\u2081 hn\u2082\n have cota\u2081 : |u n - a| < \u03b5\/2 := hNu n hn\u2081\n have cota\u2082 : |v n - b| < \u03b5\/2 := hNv n hn\u2082\n calc |(u + v) n - (a + b)|\n = |(u n + v n) - (a + b)| := by rfl\n _ = |(u n - a) + (v n - b)| := by { congr; ring }\n _ \u2264 |u n - a| + |v n - b| := by apply abs_add\n _ < \u03b5 := by linarith\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby\n intros \u03b5 h\u03b5\n cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n use max Nu Nv\n intros n hn\n cases' max_ge_iff.mp hn with hn\u2081 hn\u2082\n calc |(u + v) n - (a + b)|\n = |u n + v n - (a + b)| := by rfl\n _ = |(u n - a) + (v n - b)| := by { congr; ring }\n _ \u2264 |u n - a| + |v n - b| := by apply abs_add\n _ < \u03b5\/2 + \u03b5\/2 := add_lt_add (hNu n hn\u2081) (hNv n hn\u2082)\n _ = \u03b5 := by simp\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby\n intros \u03b5 h\u03b5\n cases' hu (\u03b5\/2) (by linarith) with Nu hNu\n cases' hv (\u03b5\/2) (by linarith) with Nv hNv\n use max Nu Nv\n intros n hn\n rw [max_ge_iff] at hn\n calc |(u + v) n - (a + b)|\n = |u n + v n - (a + b)| := by rfl\n _ = |(u n - a) + (v n - b)| := by { congr; ring }\n _ \u2264 |u n - a| + |v n - b| := by apply abs_add\n _ < \u03b5 := by linarith [hNu n (by linarith), hNv n (by linarith)]\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u a)\n (hv : limite v b)\n : limite (u + v) (a + b) :=\nby\n intros \u03b5 H\u03b5\n cases' hu (\u03b5\/2) (by linarith) with L HL\n cases' hv (\u03b5\/2) (by linarith) with M HM\n set N := max L M with _hN\n use N\n have HLN : N \u2265 L := le_max_left _ _\n have HMN : N \u2265 M := le_max_right _ _\n intros n Hn\n have H3 : |u n - a| < \u03b5\/2 := HL n (by linarith)\n have H4 : |v n - b| < \u03b5\/2 := HM n (by linarith)\n calc |(u + v) n - (a + b)|\n = |(u n + v n) - (a + b)| := by rfl\n _ = |(u n - a) + (v n - b)| := by {congr; ring }\n _ \u2264 |(u n - a)| + |(v n - b)| := by apply abs_add\n _ < \u03b5\/2 + \u03b5\/2 := by linarith\n _ = \u03b5 := by ring\n\n-- Lemas usados\n-- ============\n\n-- variable (d : \u211d)\n-- #check (abs_add a b : |a + b| \u2264 |a| + |b|)\n-- #check (add_halves a : a \/ 2 + a \/ 2 = a)\n-- #check (add_lt_add : a < b \u2192 c < d \u2192 a + c < b + d)\n-- #check (half_pos : a > 0 \u2192 a \/ 2 > 0)\n-- #check (le_max_left a b : a \u2264 max a b)\n-- #check (le_max_right a b : b \u2264 max a b)\n-- #check (le_of_max_le_left : max a b \u2264 c \u2192 a \u2264 c)\n-- #check (le_of_max_le_right : max a b \u2264 c \u2192 b \u2264 c)\n-- #check (max_le_iff : max a b \u2264 c \u2194 a \u2264 c \u2227 b \u2264 c)\n<\/pre>\nDemostraciones interactivas<\/h3>\n