Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca
Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(cuₙ\) es \(ca\).
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 : ℕ → ℝ) variable (a c : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by |
1. Demostración en lenguaje natural
Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[|cuₙ – ca| < ε] \tag{1}\]
Distinguiremos dos casos según sea \(c = 0\) o no.
Primer caso: Supongamos que \(c = 0\). Entonces, (1) se reduce a
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[|0·uₙ – 0·a| < ε] \]
es decir,
\[ (∃ N ∈ ℕ)(∀ n ≥ N)[0 < ε] \]
que se verifica para cualquier número \(N\), ya que \(ε > 0\).
Segundo caso: Supongamos que \(c ≠ 0\). Entonces, \(\dfrac{ε}{|c|}\) > 0 y, puesto que el límite de \(uₙ\) es \(a\), existe un \(k ∈ ℕ\) tal que
\[ (∀ n ≥ k)[|uₙ – a| < \frac{ε}{|c|}] \tag{2} \]
Veamos que con \(k\) se cumple (1). En efecto, sea \(n ≥ k\). Entonces,
\begin{align}
|cuₙ – ca| &= |c(uₙ – a)| \\
&= |c||uₙ – a| \\
&< |c|\frac{ε}{|c|} &&\text{[por (2)]} \\
&= ε
\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 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u v : ℕ → ℝ) variable (a c : ℝ) def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by by_cases hc : c = 0 . -- hc : c = 0 subst hc -- ⊢ limite (fun n => 0 * u n) (0 * a) intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => 0 * u n) n - 0 * a| < ε aesop . -- hc : ¬c = 0 intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε have hc' : 0 < |c| := abs_pos.mpr hc have hεc : 0 < ε / |c| := div_pos hε hc' specialize h (ε/|c|) hεc -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| cases' h with N hN -- N : ℕ -- hN : ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(fun n => c * u n) n - c * a| < ε specialize hN n hn -- hN : |u n - a| < ε / |c| dsimp only calc |c * u n - c * a| = |c * (u n - a)| := congr_arg abs (mul_sub c (u n) a).symm _ = |c| * |u n - a| := abs_mul c (u n - a) _ < |c| * (ε / |c|) := (mul_lt_mul_left hc').mpr hN _ = ε := mul_div_cancel' ε (ne_of_gt hc') -- 2ª demostración -- =============== example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by by_cases hc : c = 0 . -- hc : c = 0 subst hc -- ⊢ limite (fun n => 0 * u n) (0 * a) intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => 0 * u n) n - 0 * a| < ε aesop . -- hc : ¬c = 0 intros ε hε -- ε : ℝ -- hε : ε > 0 -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε have hc' : 0 < |c| := abs_pos.mpr hc have hεc : 0 < ε / |c| := div_pos hε hc' specialize h (ε/|c|) hεc -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| cases' h with N hN -- N : ℕ -- hN : ∀ (n : ℕ), n ≥ N → |u n - a| < ε / |c| use N -- ⊢ ∀ (n : ℕ), n ≥ N → |(fun n => c * u n) n - c * a| < ε intros n hn -- n : ℕ -- hn : n ≥ N -- ⊢ |(fun n => c * u n) n - c * a| < ε specialize hN n hn -- hN : |u n - a| < ε / |c| dsimp only -- ⊢ |c * u n - c * a| < ε rw [← mul_sub] -- ⊢ |c * (u n - a)| < ε rw [abs_mul] -- ⊢ |c| * |u n - a| < ε rw [← lt_div_iff' hc'] -- ⊢ |u n - a| < ε / |c| exact hN -- 3ª demostración -- =============== example (h : limite u a) : limite (fun n ↦ c * (u n)) (c * a) := by by_cases hc : c = 0 . subst hc intros ε hε aesop . intros ε hε have hc' : 0 < |c| := by aesop have hεc : 0 < ε / |c| := div_pos hε hc' cases' h (ε/|c|) hεc with N hN use N intros n hn specialize hN n hn dsimp only rw [← mul_sub, abs_mul, ← lt_div_iff' hc'] exact hN -- Lemas usados -- ============ -- variable (b c : ℝ) -- #check (abs_mul a b : |a * b| = |a| * |b|) -- #check (abs_pos.mpr : a ≠ 0 → 0 < |a|) -- #check (div_pos : 0 < a → 0 < b → 0 < a / b) -- #check (lt_div_iff' : 0 < c → (a < b / c ↔ c * a < b)) -- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a) -- #check (mul_lt_mul_left : 0 < a → (a * b < a * c ↔ b < c)) -- #check (mul_sub a b c : a * (b - c) = a * b - a * c) |
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 |
theory Limite_multiplicado_por_una_constante 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 a" shows "limite (λ n. c * u n) (c * a)" proof (unfold limite_def) show "∀ε>0. ∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" proof (intro allI impI) fix ε :: real assume "0 < ε" show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" proof (cases "c = 0") assume "c = 0" then show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" by (simp add: ‹0 < ε›) next assume "c ≠ 0" then have "0 < ¦c¦" by simp then have "0 < ε/¦c¦" by (simp add: ‹0 < ε›) then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε/¦c¦" using assms limite_def by auto have "∀n≥N. ¦c * u n - c * a¦ < ε" proof (intro allI impI) fix n assume "n ≥ N" have "¦c * u n - c * a¦ = ¦c * (u n - a)¦" by argo also have "… = ¦c¦ * ¦u n - a¦" by (simp only: abs_mult) also have "… < ¦c¦ * (ε/¦c¦)" using hN ‹n ≥ N› ‹0 < ¦c¦› by (simp only: mult_strict_left_mono) finally show "¦c * u n - c * a¦ < ε" using ‹0 < ¦c¦› by auto qed then show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε" by (rule exI) qed qed qed end |
