Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0
Demostrar con Lean4 que si \(uₙ\) y \(vₙ\) convergen a \(0\), entonces \(uₙvₙ\) converge a \(0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u v : ℕ → ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by sorry |
1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃N ∈ ℕ)(∀n ≥ N)[|(u·v)(n) – 0| < ε] \tag{1} \]
Puesto que el límite de \(uₙ\) es \(0\), existe un \(U ∈ ℕ\) tal que
\[ (∀n ≥ U)[|u(n) – 0| < ε] \tag{2} \]
y, puesto que el límite de \(vₙ\) es \(0\), existe un \(V ∈ ℕ\) tal que
\[ (∀n ≥ V)[|v(n) – 0| < 1] \tag{3} \]
Entonces, \(N = \text{máx}(U, V)\) cumple (1). En efecto, sea \(n ≥ N\). Entonces,
\(n ≥ U\) y \(n ≥ V\) y, aplicando (2) y (3), se tiene
\begin{align}
&|u(n) – 0| < ε \tag{4} \\
&|v(n) – 0| < 1 \tag{5}
\end{align}
Por tanto,
\begin{align}
|(u·v)(n) – 0| &= |u(n)·v(n)| \\
&= |u(n)|·|v n| \\
&< ε·1 &&\text{[por (4) y (5)]} \\
&= ε
\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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u v : ℕ → ℝ} def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε cases' hu ε hε with U hU -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε cases' hv 1 zero_lt_one with V hV -- V : ℕ -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1 let N := max U V use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(u * v) n - 0| < ε specialize hU n (le_of_max_le_left hn) -- hU : |u n - 0| < ε specialize hV n (le_of_max_le_right hn) -- hV : |v n - 0| < 1 rw [sub_zero] at * -- hU : |u n - 0| < ε -- hV : |v n - 0| < 1 -- ⊢ |(u * v) n - 0| < ε calc |(u * v) n| = |u n * v n| := rfl _ = |u n| * |v n| := abs_mul (u n) (v n) _ < ε * 1 := mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n)) _ = ε := mul_one ε -- 2ª demostración -- =============== example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε cases' hu ε hε with U hU -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε cases' hv 1 (by linarith) with V hV -- V : ℕ -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1 let N := max U V use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(u * v) n - 0| < ε specialize hU n (le_of_max_le_left hn) -- hU : |u n - 0| < ε specialize hV n (le_of_max_le_right hn) -- hV : |v n - 0| < 1 rw [sub_zero] at * -- hU : |u n| < ε -- hV : |v n| < 1 -- ⊢ |(u * v) n| < ε calc |(u * v) n| = |u n * v n| := rfl _ = |u n| * |v n| := abs_mul (u n) (v n) _ < ε * 1 := by { apply mul_lt_mul'' hU hV <;> simp [abs_nonneg] } _ = ε := mul_one ε -- 3ª demostración -- =============== example (hu : limite u 0) (hv : limite v 0) : limite (u * v) 0 := by intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε cases' hu ε hε with U hU -- U : ℕ -- hU : ∀ (n : ℕ), n ≥ U → |u n - 0| < ε cases' hv 1 (by linarith) with V hV -- V : ℕ -- hV : ∀ (n : ℕ), n ≥ V → |v n - 0| < 1 let N := max U V use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(u * v) n - 0| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(u * v) n - 0| < ε have hUN : U ≤ N := le_max_left U V have hVN : V ≤ N := le_max_right U V specialize hU n (by linarith) -- hU : |u n - 0| < ε specialize hV n (by linarith) -- hV : |v n - 0| < 1 rw [sub_zero] at * -- hU : |u n| < ε -- hV : |v n| < 1 -- ⊢ |(u * v) n| < ε rw [Pi.mul_apply] -- ⊢ |u n * v n| < ε rw [abs_mul] -- ⊢ |u n| * |v n| < ε convert mul_lt_mul'' hU hV _ _ using 2 <;> simp -- Lemas usados -- ============ -- variable (a b c d : ℝ) -- variable (I : Type _) -- variable (f : I → Type _) -- #check (zero_lt_one : 0 < 1) -- #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 (sub_zero a : a - 0 = a) -- #check (abs_mul a b : |a * b| = |a| * |b|) -- #check (mul_lt_mul'' : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d) -- #check (abs_nonneg a : 0 ≤ |a|) -- #check (mul_one a : a * 1 = a) |
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 |
theory Producto_de_sucesiones_convergentes_a_cero imports Main HOL.Real begin definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)" lemma assumes "limite u 0" "limite v 0" shows "limite (λ n. u n * v n) 0" proof (unfold limite_def; intro allI impI) fix ε :: real assume hε : "0 < ε" then obtain U where hU : "∀n≥U. ¦u n - 0¦ < ε" using assms(1) limite_def by auto obtain V where hV : "∀n≥V. ¦v n - 0¦ < 1" using hε assms(2) limite_def by fastforce have "∀n≥max U V. ¦u n * v n - 0¦ < ε" proof (intro allI impI) fix n assume hn : "max U V ≤ n" then have "U ≤ n" by simp then have "¦u n - 0¦ < ε" using hU by blast have hnV : "V ≤ n" using hn by simp then have "¦v n - 0¦ < 1" using hV by blast have "¦u n * v n - 0¦ = ¦(u n - 0) * (v n - 0)¦" by simp also have "… = ¦u n - 0¦ * ¦v n - 0¦" by (simp add: abs_mult) also have "… < ε * 1" using ‹¦u n - 0¦ < ε› ‹¦v n - 0¦ < 1› by (rule abs_mult_less) also have "… = ε" by simp finally show "¦u n * v n - 0¦ < ε" by this qed then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε" by (rule exI) qed end |
