Demostrar con Lean4 que si \(u\u2099\) y \(v\u2099\) convergen a \(0\), entonces \(u\u2099v\u2099\) converge a \(0\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable {u v : \u2115 \u2192 \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\nexample\n (hu : limite u 0)\n (hv : limite v 0)\n : limite (u * v) 0 :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(\u03b5 \u2208 \u211d\) tal que \(\u03b5 > 0\). Tenemos que demostrar que
\n\[ (\u2203N \u2208 \u2115)(\u2200n \u2265 N)[|(u\u00b7v)(n) - 0| < \u03b5] \tag{1} \]
\nPuesto que el l\u00edmite de \(u\u2099\) es \(0\), existe un \(U \u2208 \u2115\) tal que
\n\[ (\u2200n \u2265 U)[|u(n) - 0| < \u03b5] \tag{2} \]
\ny, puesto que el l\u00edmite de \(v\u2099\) es \(0\), existe un \(V \u2208 \u2115\) tal que
\n\[ (\u2200n \u2265 V)[|v(n) - 0| < 1] \tag{3} \]
\nEntonces, \(N = \text{m\u00e1x}(U, V)\) cumple (1). En efecto, sea \(n \u2265 N\). Entonces,
\n\(n \u2265 U\) y \(n \u2265 V\) y, aplicando (2) y (3), se tiene
\n\begin{align}
\n &|u(n) - 0| < \u03b5 \tag{4} \\
\n &|v(n) - 0| < 1 \tag{5}
\n\end{align}
\nPor tanto,
\n\begin{align}
\n |(u\u00b7v)(n) - 0| &= |u(n)\u00b7v(n)| \\
\n &= |u(n)|\u00b7|v n| \\
\n &< \u03b5\u00b71 &&\text{[por (4) y (5)]} \\
\n &= \u03b5
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable {u v : \u2115 \u2192 \u211d}\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n fun u c \u21a6 \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| < \u03b5\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u 0)\n (hv : limite v 0)\n : limite (u * v) 0 :=\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 - 0| < \u03b5\n cases' hu \u03b5 h\u03b5 with U hU\n -- U : \u2115\n -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - 0| < \u03b5\n cases' hv 1 zero_lt_one with V hV\n -- V : \u2115\n -- hV : \u2200 (n : \u2115), n \u2265 V \u2192 |v n - 0| < 1\n let N := max U V\n use N\n -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 N\n -- \u22a2 |(u * v) n - 0| < \u03b5\n specialize hU n (le_of_max_le_left hn)\n -- hU : |u n - 0| < \u03b5\n specialize hV n (le_of_max_le_right hn)\n -- hV : |v n - 0| < 1\n rw [sub_zero] at *\n -- hU : |u n - 0| < \u03b5\n -- hV : |v n - 0| < 1\n -- \u22a2 |(u * v) n - 0| < \u03b5\n calc |(u * v) n|\n = |u n * v n| := rfl\n _ = |u n| * |v n| := abs_mul (u n) (v n)\n _ < \u03b5 * 1 := mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))\n _ = \u03b5 := mul_one \u03b5\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u 0)\n (hv : limite v 0)\n : limite (u * v) 0 :=\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 - 0| < \u03b5\n cases' hu \u03b5 h\u03b5 with U hU\n -- U : \u2115\n -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - 0| < \u03b5\n cases' hv 1 (by linarith) with V hV\n -- V : \u2115\n -- hV : \u2200 (n : \u2115), n \u2265 V \u2192 |v n - 0| < 1\n let N := max U V\n use N\n -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 N\n -- \u22a2 |(u * v) n - 0| < \u03b5\n specialize hU n (le_of_max_le_left hn)\n -- hU : |u n - 0| < \u03b5\n specialize hV n (le_of_max_le_right hn)\n -- hV : |v n - 0| < 1\n rw [sub_zero] at *\n -- hU : |u n| < \u03b5\n -- hV : |v n| < 1\n -- \u22a2 |(u * v) n| < \u03b5\n calc |(u * v) n|\n = |u n * v n| := rfl\n _ = |u n| * |v n| := abs_mul (u n) (v n)\n _ < \u03b5 * 1 := by { apply mul_lt_mul'' hU hV <;> simp [abs_nonneg] }\n _ = \u03b5 := mul_one \u03b5\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hu : limite u 0)\n (hv : limite v 0)\n : limite (u * v) 0 :=\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 - 0| < \u03b5\n cases' hu \u03b5 h\u03b5 with U hU\n -- U : \u2115\n -- hU : \u2200 (n : \u2115), n \u2265 U \u2192 |u n - 0| < \u03b5\n cases' hv 1 (by linarith) with V hV\n -- V : \u2115\n -- hV : \u2200 (n : \u2115), n \u2265 V \u2192 |v n - 0| < 1\n let N := max U V\n use N\n -- \u22a2 \u2200 (n : \u2115), n \u2265 N \u2192 |(u * v) n - 0| < \u03b5\n intros n hn\n -- n : \u2115\n -- hn : n \u2265 N\n -- \u22a2 |(u * v) n - 0| < \u03b5\n have hUN : U \u2264 N := le_max_left U V\n have hVN : V \u2264 N := le_max_right U V\n specialize hU n (by linarith)\n -- hU : |u n - 0| < \u03b5\n specialize hV n (by linarith)\n -- hV : |v n - 0| < 1\n rw [sub_zero] at *\n -- hU : |u n| < \u03b5\n -- hV : |v n| < 1\n -- \u22a2 |(u * v) n| < \u03b5\n rw [Pi.mul_apply]\n -- \u22a2 |u n * v n| < \u03b5\n rw [abs_mul]\n -- \u22a2 |u n| * |v n| < \u03b5\n convert mul_lt_mul'' hU hV _ _ using 2 <;> simp\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c d : \u211d)\n-- variable (I : Type _)\n-- variable (f : I \u2192 Type _)\n-- #check (zero_lt_one : 0 < 1)\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 (sub_zero a : a - 0 = a)\n-- #check (abs_mul a b : |a * b| = |a| * |b|)\n-- #check (mul_lt_mul'' : a < c \u2192 b < d \u2192 0 \u2264 a \u2192 0 \u2264 b \u2192 a * b < c * d)\n-- #check (abs_nonneg a : 0 \u2264 |a|)\n-- #check (mul_one a : a * 1 = a)\n<\/pre>\n