Análisis – Página 3

Suma de los primeros cubos

PorJosé A. Alonso 22 septiembre 202117 septiembre 2021

Demostrar que la suma de los primeros cubos

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

1	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

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

[expand title=»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

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>
[/expand]

[expand title=»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

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

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

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>
[/expand]

Suma de los primeros cuadrados

PorJosé A. Alonso 21 septiembre 202116 septiembre 2021

Demostrar que la suma de los primeros cuadrados

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

1	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

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

[expand title=»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

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>
[/expand]

[expand title=»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

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

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

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>
[/expand]

Suma de progresión geométrica

PorJosé A. Alonso 20 septiembre 202120 septiembre 2021

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

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

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

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

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

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»]

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

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»]

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

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

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

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]

Suma de progresión aritmética

PorJosé A. Alonso 19 septiembre 202115 septiembre 2021

Demostrar que la suma de los términos de la progresión aritmética

   a + (a + d) + (a + 2 × d) + ··· + (a + n × d)

1	a + (a + d) + (a + 2 × d) + ··· + (a + n × d)

es (n + 1) × (2 × a + n × d) / 2.

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

import data.real.basic
open nat

variable  (n : ℕ)
variables (a d : ℝ)

@[simp]
def sumaPA : ℝ → ℝ → ℕ → ℝ
| a d 0       := a
| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :
  2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=
sorry

import data.real.basic

open nat

variable (n : ℕ)

variables (a d : ℝ)

@[simp]

def sumaPA : ℝ → ℝ → ℕ → ℝ

| a d 0 := a

| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :

2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  (n : ℕ)
variables (a d : ℝ)

set_option pp.structure_projections false

@[simp]
def sumaPA : ℝ → ℝ → ℕ → ℝ
| a d 0       := a
| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :
  2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=
begin
  induction n with n HI,
  { simp, },
  { calc 2 * sumaPA a d (succ n)
         = 2 * (sumaPA a d n + (a + (n + 1) * d))
           : rfl
     ... = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)
           : by ring_nf
     ... = ((n + 1) * (2 * a + n * d)) + 2 * (a + (n + 1) * d)
           : by {congr; rw HI}
     ... = (n + 2) * (2 * a + (n + 1) * d)
           : by ring_nf
     ... = (succ n + 1) * (2 * a + succ n * d)
           : congr_arg2 (*) (by norm_cast) rfl, },
end

import data.real.basic

open nat

variable (n : ℕ)

variables (a d : ℝ)

set_option pp.structure_projections false

@[simp]

def sumaPA : ℝ → ℝ → ℕ → ℝ

| a d 0 := a

| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :

2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=

begin

induction n with n HI,

{ simp, },

{ calc 2 * sumaPA a d (succ n)

= 2 * (sumaPA a d n + (a + (n + 1) * d))

: rfl

... = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)

: by ring_nf

... = ((n + 1) * (2 * a + n * d)) + 2 * (a + (n + 1) * d)

: by {congr; rw HI}

... = (n + 2) * (2 * a + (n + 1) * d)

: by ring_nf

... = (succ n + 1) * (2 * a + succ n * d)

: congr_arg2 (*) (by norm_cast) rfl, },

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»]

theory Suma_de_progresion_aritmetica
imports Main HOL.Real
begin

fun sumaPA :: "real ⇒ real ⇒ nat ⇒ real" where
  "sumaPA a d 0 = a"
| "sumaPA a d (Suc n) = sumaPA a d n + (a + (n + 1) * d)"

(* 1ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2 * a + n * d)"
proof (induct n)
  show "2 * sumaPA a d 0 =
        (real 0 + 1) * (2 * a + real 0 * d)"
    by simp
next
  fix n
  assume HI : "2 * sumaPA a d n =
               (n + 1) * (2 * a + n * d)"
  have "2 * sumaPA a d (Suc n) =
        2 * (sumaPA a d n + (a + (n + 1) * d))"
    by simp
  also have "… = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)"
    by simp
  also have "… = (n + 1) * (2 * a + n * d) + 2 * (a + (n + 1) * d)"
    using HI by simp
  also have "… = (real (Suc n) + 1) * (2 * a + (Suc n) * d)"
    by (simp add: algebra_simps)
  finally show "2 * sumaPA a d (Suc n) =
                (real (Suc n) + 1) * (2 * a + (Suc n) * d)"
    by this
qed

(* 2ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2*a + n*d)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by (simp add: algebra_simps)
qed

(* 3ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2*a + n*d)"
by (induct n) (simp_all add: algebra_simps)

end

theory Suma_de_progresion_aritmetica

imports Main HOL.Real

begin

fun sumaPA :: "real ⇒ real ⇒ nat ⇒ real" where

"sumaPA a d 0 = a"

| "sumaPA a d (Suc n) = sumaPA a d n + (a + (n + 1) * d)"

(* 1ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2 * a + n * d)"

proof (induct n)

show "2 * sumaPA a d 0 =

(real 0 + 1) * (2 * a + real 0 * d)"

by simp

fix n

assume HI : "2 * sumaPA a d n =

(n + 1) * (2 * a + n * d)"

have "2 * sumaPA a d (Suc n) =

2 * (sumaPA a d n + (a + (n + 1) * d))"

by simp

also have "… = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)"

by simp

also have "… = (n + 1) * (2 * a + n * d) + 2 * (a + (n + 1) * d)"

using HI by simp

also have "… = (real (Suc n) + 1) * (2 * a + (Suc n) * d)"

by (simp add: algebra_simps)

finally show "2 * sumaPA a d (Suc n) =

(real (Suc n) + 1) * (2 * a + (Suc n) * d)"

by this

qed

(* 2ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2*a + n*d)"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by (simp add: algebra_simps)

qed

(* 3ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2*a + n*d)"

by (induct n) (simp_all add: 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]

Si f es continua en a y el límite de u(n) es a, entonces el límite de f(u(n)) es f(a)

PorJosé A. Alonso 17 septiembre 202114 septiembre 2021

En Lean, se puede definir que a es el límite de la sucesión u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, \|u n - a\| < ε

y que f es continua en a por

   def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

1 2	def continua_en_punto (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, \|x - a\| ≤ δ → \|f x - f a\| ≤ ε

Demostrar que si f es continua en a y el límite de uₙ es a, entonces el límite de f(uₙ) es f(a).

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

import data.real.basic

variable {f : ℝ → ℝ}
variable {a : ℝ}
variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
sorry

import data.real.basic

variable {f : ℝ → ℝ}

variable {a : ℝ}

variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable {f : ℝ → ℝ}
variable {a : ℝ}
variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

-- 1ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,
  cases hu δ hδ1 with k hk,
  use k,
  intros n hn,
  apply hδ2,
  exact hk n hn,
end

-- 2ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,
  cases hu δ hδ1 with k hk,
  exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,
end

-- 3ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε,
  obtain ⟨k, hk⟩ := hu δ hδ1,
  exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,
end

import data.real.basic

variable {f : ℝ → ℝ}

variable {a : ℝ}

variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

-- 1ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,

cases hu δ hδ1 with k hk,

use k,

intros n hn,

apply hδ2,

exact hk n hn,

end

-- 2ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,

cases hu δ hδ1 with k hk,

exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,

end

-- 3ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε,

obtain ⟨k, hk⟩ := hu δ hδ1,

exact ⟨k, λ n hn, hδ2 (u n) (hk n 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»]

theory CS_de_continuidad
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where
  "continua_en_punto f a ⟷
   (∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

(* 1ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
  proof (intro allI impI)
    fix n
    assume "n ≥ k"
    then have "¦u n - a¦ ≤ δ"
      using hk by auto
    then show "¦(f ∘ u) n - f a¦ ≤ ε"
      using hδ2 by simp
  qed
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    by auto
qed

(* 2ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hk hδ2 by simp
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    by auto
qed

(* 3ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hk hδ2 by auto
qed

(* 4ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where
              hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def by auto
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hδ by auto
qed

(* 5ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
  using assms continua_en_punto_def limite_def
  by force

end

theory CS_de_continuidad

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where

"continua_en_punto f a ⟷

(∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

(* 1ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def hδ1 by auto

have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

proof (intro allI impI)

fix n

assume "n ≥ k"

then have "¦u n - a¦ ≤ δ"

using hk by auto

then show "¦(f ∘ u) n - f a¦ ≤ ε"

using hδ2 by simp

qed

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

by auto

qed

(* 2ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def hδ1 by auto

have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hk hδ2 by simp

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

by auto

qed

(* 3ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def hδ1 by auto

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hk hδ2 by auto

qed

(* 4ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where

hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def by auto

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hδ by auto

qed

(* 5ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

using assms continua_en_punto_def limite_def

by force

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]