Suma de progresión geométrica
Demostrar que la suma de los términos de la progresión geométrica
1 |
a + aq + aq² + ··· + aqnⁿ |
es
1 2 3 |
a(1 - qⁿ⁺¹) ------------- 1 - q |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import data.real.basic open nat variable (n : ℕ) variables (a q : ℝ) def sumaPG : ℝ → ℝ → ℕ → ℝ | a q 0 := a | a q (n + 1) := sumaPG a q n + (a * q^(n + 1)) example : (1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) := 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 |
import data.real.basic open nat variable (n : ℕ) variables (a q : ℝ) set_option pp.structure_projections false @[simp] def sumaPG : ℝ → ℝ → ℕ → ℝ | a q 0 := a | a q (n + 1) := sumaPG a q n + (a * q^(n + 1)) example : (1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) := begin induction n with n HI, { simp, ac_refl, }, { calc (1 - q) * sumaPG a q (succ n) = (1 - q) * (sumaPG a q n + (a * q^(n + 1))) : rfl ... = (1 - q) * sumaPG a q n + (1 - q) * (a * q^(n + 1)) : by ring_nf ... = a * (1 - q ^ (n + 1)) + (1 - q) * (a * q^(n + 1)) : by {congr ; rw HI} ... = a * (1 - q ^ (succ n + 1)) : by ring_nf }, 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 52 53 54 55 56 57 58 59 60 61 62 63 |
theory Suma_de_progresion_geometrica imports Main HOL.Real begin fun sumaPG :: "real ⇒ real ⇒ nat ⇒ real" where "sumaPG a q 0 = a" | "sumaPG a q (Suc n) = sumaPG a q n + (a * q^(n + 1))" (* 1ª demostración *) lemma "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))" proof (induct n) show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))" by simp next fix n assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))" have "(1 - q) * sumaPG a q (Suc n) = (1 - q) * (sumaPG a q n + (a * q^(n + 1)))" by simp also have "… = (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)" by (simp add: algebra_simps) also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)" using HI by simp also have "… = a * (1 - q ^ (n + 1) + (1 - q) * q^(n + 1))" by (simp add: algebra_simps) also have "… = a * (1 - q ^ (n + 1) + q^(n + 1) - q^(n + 2))" by (simp add: algebra_simps) also have "… = a * (1 - q^(n + 2))" by simp also have "… = a * (1 - q ^ (Suc n + 1))" by simp finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))" by this qed (* 2ª demostración *) lemma "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))" proof (induct n) show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))" by simp next fix n assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))" have "(1 - q) * sumaPG a q (Suc n) = (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)" by (simp add: algebra_simps) also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)" using HI by simp also have "… = a * (1 - q ^ (n + 1) + q^(n + 1) - q^(n + 2))" by (simp add: algebra_simps) finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))" by simp qed (* 3ª demostración *) lemma "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))" using power_add by (induct n) (auto simp: algebra_simps) 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]