Menu Close

Categoría: Análisis

Suma de potencias de dos

Demostrar que

   1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1

Para ello, completar la siguiente teoría de Lean:

import algebra.big_operators
import tactic
open finset nat
 
open_locale big_operators
 
variable (n : )
 
example :
  ∑ k in range n, 2^k = 2^n - 1 :=
sorry
Soluciones con Lean
import algebra.big_operators
import tactic
open finset nat
 
open_locale big_operators
set_option pp.structure_projections false
 
variable (n : )
 
example :
  ∑ k in range n, 2^k = 2^n - 1 :=
begin
  induction n with n HI,
  { simp, },
  { calc ∑ k in range (succ n), 2^k
         = ∑ k in range n, 2^k + 2^n
             : sum_range_succ (λ x, 2 ^ x) n
     ... = (2^n - 1) + 2^n
             : congr_arg2 (+) HI rfl
     ... = (2^n + 2^n) - 1
             : by omega
     ... = 2^n * 2 - 1
             : by {congr; simp}
     ... = 2^(succ n) - 1
             : by {congr' 1; 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>

Soluciones con Isabelle/HOL
theory Suma_de_potencias_de_dos
imports Main
begin
 
(* 1ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (∑k≤n. (2::nat)^k) + 2^Suc n"
    by simp
  also have "… = (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  also have "… = 2^(Suc n + 1) - 1"
    by simp
  finally show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" .
qed
 
(* 2ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  then show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1"
    by simp
qed
 
(* 3ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed
 
(* 4ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
by (induct n) simp_all

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Fórmula de Gauss de la suma de los primeros números naturales

La fórmula de Gauss para la suma de los primeros números naturales es

   0 + 1 + 2 + ... + (n-1) = n(n-1)/2

En un ejercicio anterior se ha demostrado dicha fórmula por inducción. Otra forma de demostrarla, sin usar inducción, es la siguiente: La suma se puede escribir de dos maneras

   S = 0     + 1     + 2     + ... + (n-3) + (n-2) + (n-1)
   S = (n-1) + (n-2) + (n-3) + ... + 2     + 1     + 0

Al sumar, se observa que cada par de números de la misma columna da como suma (n-1), y puesto que hay n columnas en total, se sigue

   2S = n(n-1)

lo que prueba la fórmula.

Demostrar la fórmula de Gauss siguiendo el procedimiento anterior.

Para ello, completar la siguiente teoría de Lean:

import algebra.big_operators.basic
import algebra.big_operators.intervals
 
open_locale big_operators
open finset nat
 
variables (n i : )
 
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
sorry
Soluciones con Lean
import algebra.big_operators.basic
import algebra.big_operators.intervals
 
open_locale big_operators
open finset nat
 
variables (n i : )
 
-- Lema auxiliar
-- =============
 
-- Se usará el siguiente lema auxiliar del que se presentan distintas
-- demostraciones.
 
-- 1ª demostración del lema auxiliar
example :  x, x ∈ range n  x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  replace hx : x < n := mem_range.1 hx,
  replace hx : x  n - 1 := le_pred_of_lt hx,
  exact nat.add_sub_cancel' hx,
end
 
-- 2ª demostración del lema auxiliar
example :  x, x ∈ range n  x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),
end
 
-- 3ª demostración del lema auxiliar
lemma auxiliar :  x, x ∈ range n  x + (n - 1 - x) = n - 1 :=
λ x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))
 
-- Lema principal
-- ==============
 
-- 1ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, i)
         : mul_two _
 ... = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : congr_arg2 (+) rfl (sum_range_reflect id n).symm
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = card (range n)(n - 1)
         : sum_const (n - 1)
 ... = card (range n) * (n - 1)
         : nat.nsmul_eq_mul _ _
 ... = n * (n - 1)
         : congr_arg2 (*) (card_range n) rfl
 
-- 2ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : by rw [sum_range_reflect (λ i, i) n, mul_two]
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = n * (n - 1)
         : by rw [sum_const, card_range, nat.nsmul_eq_mul]

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>

Soluciones con Isabelle/HOL
theory Formula_de_Gauss_de_la_suma
imports Main
begin
 
lemma
  fixes n :: nat
  shows "2 * (∑i<n. i) = n * (n - 1)"
proof -
  have "2 * (∑i<n. i) = (∑i<n. i) + (∑i<n. i)"
    by simp
  also have "… = (∑i<n. i) + (∑i<n. n - Suc i)"
    using sum.nat_diff_reindex [where g = id] by auto
  also have "… = (∑i<n. (i + (n - Suc i)))"
    using sum.distrib [where A = "{..<n}" and
                             g = id and
                             h = "λi. n - Suc i"] by auto
  also have "… = (∑i<n. n - 1)"
    by simp
  also have "… = n * (n -1)"
    using sum_constant by auto
  finally show "2 * (∑i<n. i) = n * (n - 1)" .
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>

Suma de los primeros cubos

Demostrar que la suma de los primeros cubos

   0³ + 1³ + 2³ + 3³ + ··· + n³

es (n(n+1)/2)²

Para ello, completar la siguiente teoría de Lean:

import data.nat.basic
import tactic
open nat
 
variable (n : )
 
def sumaCubos :   
| 0     := 0
| (n+1) := sumaCubos n + (n+1)^3
 
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
sorry
Soluciones con Lean
import data.nat.basic
import tactic
open nat
 
variable (n : )
 
set_option pp.structure_projections false
 
@[simp]
def sumaCubos :   
| 0     := 0
| (n+1) := sumaCubos n + (n+1)^3
 
-- 1ª demostración
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
begin
  induction n with n HI,
  { simp,
    ring, },
  { calc 4 * sumaCubos (succ n)
         = 4 * (sumaCubos n + (n+1)^3)
           : by simp
     ... = 4 * sumaCubos n + 4*(n+1)^3
           : by ring
     ... = (n*(n+1))^2 + 4*(n+1)^3
           : by {congr; rw HI}
     ... = (n+1)^2*(n^2+4*n+4)
           : by ring
     ... = (n+1)^2*(n+2)^2
           : by ring
     ... = ((n+1)*(n+2))^2
           : by ring
     ... = (succ n * (succ n + 1)) ^ 2
           : by simp, },
end
 
-- 2ª demostración
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
begin
  induction n with n HI,
  { simp,
    ring, },
  { calc 4 * sumaCubos (succ n)
         = 4 * sumaCubos n + 4*(n+1)^3
           : by {simp ; ring}
     ... = (n*(n+1))^2 + 4*(n+1)^3
           : by {congr; rw HI}
     ... = ((n+1)*(n+2))^2
           : by ring
     ... = (succ n * (succ n + 1)) ^ 2
           : by simp, },
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>

Soluciones con Isabelle/HOL
theory Suma_de_los_primeros_cubos
imports Main
begin
 
fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0       = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"
 
(* 1ª demostración *)
lemma
  "4 * sumaCubos n = (n*(n+1))^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0 * (0 + 1))^2"
    by simp
next
  fix n
  assume HI : "4 * sumaCubos n = (n * (n + 1))^2"
  have "4 * sumaCubos (Suc n) = 4 * (sumaCubos n + (n+1)^3)"
    by simp
  also have "… = 4 * sumaCubos n + 4*(n+1)^3"
    by simp
  also have "… = (n*(n+1))^2 + 4*(n+1)^3"
    using HI by simp
  also have "… = (n+1)^2*(n^2+4*n+4)"
    by algebra
  also have "… = (n+1)^2*(n+2)^2"
    by algebra
  also have "… = ((n+1)*((n+1)+1))^2"
    by algebra
  also have "… = (Suc n * (Suc n + 1))^2"
    by (simp only: Suc_eq_plus1)
  finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2"
    by this
qed
 
(* 2ª demostración *)
lemma
  "4 * sumaCubos n = (n*(n+1))^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0 * (0 + 1))^2"
    by simp
next
  fix n
  assume HI : "4 * sumaCubos n = (n * (n + 1))^2"
  have "4 * sumaCubos (Suc n) = 4 * sumaCubos n + 4*(n+1)^3"
    by simp
  also have "… = (n*(n+1))^2 + 4*(n+1)^3"
    using HI by simp
  also have "… = ((n+1)*((n+1)+1))^2"
    by algebra
  also have "… = (Suc n * (Suc n + 1))^2"
    by (simp only: Suc_eq_plus1)
  finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2" .
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>

Suma de los primeros cuadrados

Demostrar que la suma de los primeros cuadrados

   0² + 1² + 2² + 3² + ··· + n²

es n(n+1)(2n+1)/6.

Para ello, completar la siguiente teoría de Lean:

import data.nat.basic
import tactic
open nat
 
variable (n : )
 
@[simp]
def sumaCuadrados :   
| 0     := 0
| (n+1) := sumaCuadrados n + (n+1)^2
 
example :
  6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=
sorry
Soluciones con Lean
import data.nat.basic
import tactic
open nat
 
variable (n : )
 
set_option pp.structure_projections false
 
@[simp]
def sumaCuadrados :   
| 0     := 0
| (n+1) := sumaCuadrados n + (n+1)^2
 
-- 1ª demostración
example :
  6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=
begin
  induction n with n HI,
  { simp, },
  { calc 6 * sumaCuadrados (succ n)
         = 6 * (sumaCuadrados n + (n+1)^2)
           : by simp
     ... = 6 * sumaCuadrados n + 6 * (n+1)^2
           : by ring_nf
     ... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2
           : by {congr; rw HI}
     ... = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))
           : by ring_nf
     ... = (n + 1) * (2 * n^2 + 7 * n + 6)
           : by ring_nf
     ... = (n + 1) * (n + 2) * (2 * n + 3)
           : by ring_nf
     ... = succ n * (succ n + 1) * (2 * succ n + 1)
           : by refl, },
end
 
-- 2ª demostración
example :
  6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) :=
begin
  induction n with n HI,
  { simp, },
  { calc 6 * sumaCuadrados (succ n)
         = 6 * (sumaCuadrados n + (n+1)^2)
           : by simp
     ... = 6 * sumaCuadrados n + 6 * (n+1)^2
           : by ring_nf
     ... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2
           : by {congr; rw HI}
     ... = (n + 1) * (n + 2) * (2 * n + 3)
           : by ring_nf
     ... = succ n * (succ n + 1) * (2 * succ n + 1)
           : by refl, },
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>

Soluciones con Isabelle/HOL
theory Suma_de_los_primeros_cuadrados
imports Main
begin
 
fun sumaCuadrados :: "nat ⇒ nat" where
  "sumaCuadrados 0       = 0"
| "sumaCuadrados (Suc n) = sumaCuadrados n + (Suc n)^2"
 
(* 1ª demostración *)
lemma
  "6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)"
proof (induct n)
  show "6 * sumaCuadrados 0 =  0 * (0 + 1) * (2 * 0 + 1)"
    by simp
next
  fix n
  assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)"
  have "6 * sumaCuadrados (Suc n) =
        6 * (sumaCuadrados n + (n + 1)^2)"
    by simp
  also have "… = 6 * sumaCuadrados n + 6 * (n + 1)^2"
    by simp
  also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2"
    using HI by simp
  also have "… = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))"
    by algebra
  also have "… = (n + 1) * (2 * n^2 + 7 * n + 6)"
    by algebra
  also have "… = (n + 1) * (n + 2) * (2 * n + 3)"
    by algebra
  also have "… = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1)"
    by algebra
  also have "… = Suc n * (Suc n + 1) * (2 * Suc n + 1)"
    by (simp only: Suc_eq_plus1)
  finally show "6 * sumaCuadrados (Suc n) =
        Suc n * (Suc n + 1) * (2 * Suc n + 1)"
    by this
qed
 
(* 2ª demostración *)
lemma
  "6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)"
proof (induct n)
  show "6 * sumaCuadrados 0 =  0 * (0 + 1) * (2 * 0 + 1)"
    by simp
next
  fix n
  assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)"
  have "6 * sumaCuadrados (Suc n) =
        6 * sumaCuadrados n + 6 * (n + 1)^2"
    by simp
  also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2"
    using HI by simp
  also have "… = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1)"
    by algebra
  finally show "6 * sumaCuadrados (Suc n) =
        Suc n * (Suc n + 1) * (2 * Suc n + 1)"
    by (simp only: Suc_eq_plus1)
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>

Suma de progresión geométrica

Demostrar que la suma de los términos de la progresión geométrica

   a + aq + aq² + ··· + aqnⁿ

es

     a(1 - qⁿ⁺¹)
    -------------
       1 - q

Para ello, completar la siguiente teoría de Lean:

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
Soluciones con Lean
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>

Soluciones con Isabelle/HOL
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>