Límite multiplicado por una constante
En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.
Se define que a es el límite de la sucesión u, por
1 2 |
def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε |
donde se usa la notación |x| para el valor absoluto de x
1 |
notation `|`x`|` := abs x |
Demostrar que si el límite de u(i) es a, entonces el de c·u(i) es c·a.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import data.real.basic import tactic variables (u v : ℕ → ℝ) variables (a c : ℝ) notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε example (h : limite u a) : limite (λ n, c * (u n)) (c * a) := sorry |
[expand title=»Soluciones con Lean»]
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 |
import data.real.basic import tactic variables (u v : ℕ → ℝ) variables (a c : ℝ) notation `|`x`|` := abs x def limite : (ℕ → ℝ) → ℝ → Prop := λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε -- 1ª demostración -- =============== example (h : limite u a) : limite (λ n, c * (u n)) (c * a) := begin by_cases hc : c = 0, { subst hc, intros ε hε, by finish, }, { intros ε hε, have hc' : 0 < |c| := abs_pos.mpr hc, have hεc : 0 < ε / |c| := div_pos hε hc', specialize h (ε/|c|) hεc, cases h with N hN, use N, intros n hn, specialize hN n hn, dsimp only, rw ← mul_sub, rw abs_mul, rw ← lt_div_iff' hc', exact hN, } end -- 2ª demostración -- =============== example (h : limite u a) : limite (λ n, c * (u n)) (c * a) := begin by_cases hc : c = 0, { subst hc, intros ε hε, by finish, }, { intros ε hε, have hc' : 0 < |c| := by finish, 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, } end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones 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 |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]