Análisis – Página 2

Unicidad del límite de las sucesiones convergentes

PorJosé A. Alonso 6 febrero 202419 febrero 2024

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

   def limite : (ℕ → ℝ) → ℝ → Prop :=
     fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

1 2	def limite : (ℕ → ℝ) → ℝ → Prop := fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, \|u n - c\| < ε

Demostrar con Lean4 que cada sucesión tiene como máximo un límite.

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

import Mathlib.Data.Real.Basic
variable {u : ℕ → ℝ}
variable {a b : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
  by sorry

import Mathlib.Data.Real.Basic

variable {u : ℕ → ℝ}

variable {a b : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=

fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que si \(u\) es una sucesión y \(a\) y \(b\) son límites de \(u\), entonces \(a = b\). Para ello, basta demostrar que \(a ≤ b\) y \(b ≤ a\).

Demostraremos que \(b ≤ a\) por reducción al absurdo. Supongamos que \(b ≰ a\). Sea \(ε = b – a\). Entonces, ε/2 > 0 y, puesto que \(a\) es un límite de \(u\), existe un \(A ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ A → |u(n) – a| < \frac{ε}{2}\right] \tag{1} \]
y, puesto que \(b\) también es un límite de \(u\), existe un \(B ∈ ℕ\) tal que
\[ (∀n ∈ ℕ)\left[n ≥ B → |u(n) – b| < \frac{ε}{2}\right] \tag{2} \]
Sea \(N = máx(A, B)\). Entonces, \(N ≥ A\) y \(N ≥ B\) y, por (2) y (3), se tiene
\begin{align}
|u(N) – a| &< \frac{ε}{2} \tag{3} \\
|u(N) – b| &< \frac{ε}{2} \tag{4}
\end{align}
Para obtener una contradicción basta probar que \(ε < ε\). Su prueba es
\begin{align}
ε &= b – a \\
&= |b – a| \\
&= |(b – a) + (u(N) – u(N))| \\
&= |(u(N) – a) + (b – u(N))| \\
&≤ |u(N) – a| + |b – u(N)| \\
&= |u(N) – a| + |u(N) – b| \\
&< \frac{ε}{2} + \frac{ε}{2} && \text{[por (3) y (4)]} \\
&= ε
\end{align}

La demostración de \(a ≤ b\) es análoga a la anterior.

2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable {u : ℕ → ℝ}
variable {a b : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración del lema auxiliar
-- =================================

example
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
by
  by_contra h
  -- h : ¬b ≤ a
  -- ⊢ False
  let ε := b - a
  have hε : ε > 0 := sub_pos.mpr (not_le.mp h)
  have hε2 : ε / 2 > 0 := half_pos hε
  cases' ha (ε/2) hε2 with A hA
  -- A : ℕ
  -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2
  cases' hb (ε/2) hε2 with B hB
  -- B : ℕ
  -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2
  let N := max A B
  have hAN : A ≤ N := le_max_left A B
  have hBN : B ≤ N := le_max_right A B
  specialize hA N hAN
  -- hA : |u N - a| < ε / 2
  specialize hB N hBN
  -- hB : |u N - b| < ε / 2
  have h2 : ε < ε := by calc
    ε = b - a                   := rfl
    _ = |b - a|                 := (abs_of_pos hε).symm
    _ = |(b - a) + 0|           := by {congr ; exact (add_zero (b - a)).symm}
    _ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm}
    _ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring)
    _ ≤ |u N - a| + |b - u N|   := abs_add (u N - a) (b - u N)
    _ = |u N - a| + |u N - b|   := congrArg (|u N - a| + .) (abs_sub_comm b (u N))
    _ < ε / 2 + ε / 2           := add_lt_add hA hB
    _ = ε                       := add_halves ε
  have h3 : ¬(ε < ε) := lt_irrefl ε
  show False
  exact h3 h2

-- 2ª demostración del lema auxiliar
-- =================================

lemma aux
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
by
  by_contra h
  -- h : ¬b ≤ a
  -- ⊢ False
  let ε := b - a
  cases' ha (ε/2) (by linarith) with A hA
  -- A : ℕ
  -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2
  cases' hb (ε/2) (by linarith) with B hB
  -- B : ℕ
  -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2
  let N := max A B
  have hAN : A ≤ N := le_max_left A B
  have hBN : B ≤ N := le_max_right A B
  specialize hA N hAN
  -- hA : |u N - a| < ε / 2
  specialize hB N hBN
  -- hB : |u N - b| < ε / 2
  rw [abs_lt] at hA hB
  -- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2
  -- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2
  linarith

-- 1ª demostración
-- ===============

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (aux hb ha) (aux ha hb)

-- Lemas usados
-- ============

-- variable (c d : ℝ)
-- #check (not_le : ¬a ≤ b ↔ b < a)
-- #check (sub_pos : 0 < a - b ↔ b < a)
-- #check (half_pos : a > 0 → a / 2 > 0)
-- #check (le_max_left a b : a ≤ max a b)
-- #check (le_max_right a b : b ≤ max a b)
-- #check (abs_lt : |a| < b ↔ -b < a ∧ a < b)
-- #check (abs_of_pos : 0 < a → |a| = a)
-- #check (add_zero a : a + 0 = a)
-- #check (sub_self a : a - a = 0)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (abs_sub_comm a b : |a - b| = |b - a|)
-- #check (add_lt_add : a < b → c < d → a + c < b + d)
-- #check (add_halves a : a / 2 + a / 2 = a)
-- #check (lt_irrefl a : ¬a < a)
-- #check (le_antisymm : a ≤ b → b ≤ a → a = b)

100

101

102

103

104

105

106

import Mathlib.Data.Real.Basic

variable {u : ℕ → ℝ}

variable {a b : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=

fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración del lema auxiliar

-- =================================

example

(ha : limite u a)

(hb : limite u b)

: b ≤ a :=

by_contra h

-- h : ¬b ≤ a

-- ⊢ False

let ε := b - a

have hε : ε > 0 := sub_pos.mpr (not_le.mp h)

have hε2 : ε / 2 > 0 := half_pos hε

cases' ha (ε/2) hε2 with A hA

-- A : ℕ

-- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2

cases' hb (ε/2) hε2 with B hB

-- B : ℕ

-- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2

let N := max A B

have hAN : A ≤ N := le_max_left A B

have hBN : B ≤ N := le_max_right A B

specialize hA N hAN

-- hA : |u N - a| < ε / 2

specialize hB N hBN

-- hB : |u N - b| < ε / 2

have h2 : ε < ε := by calc

ε = b - a := rfl

_ = |b - a| := (abs_of_pos hε).symm

_ = |(b - a) + 0| := by {congr ; exact (add_zero (b - a)).symm}

_ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm}

_ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring)

_ ≤ |u N - a| + |b - u N| := abs_add (u N - a) (b - u N)

_ = |u N - a| + |u N - b| := congrArg (|u N - a| + .) (abs_sub_comm b (u N))

_ < ε / 2 + ε / 2 := add_lt_add hA hB

_ = ε := add_halves ε

have h3 : ¬(ε < ε) := lt_irrefl ε

show False

exact h3 h2

-- 2ª demostración del lema auxiliar

-- =================================

lemma aux

(ha : limite u a)

(hb : limite u b)

: b ≤ a :=

by_contra h

-- h : ¬b ≤ a

-- ⊢ False

let ε := b - a

cases' ha (ε/2) (by linarith) with A hA

-- A : ℕ

-- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2

cases' hb (ε/2) (by linarith) with B hB

-- B : ℕ

-- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2

let N := max A B

have hAN : A ≤ N := le_max_left A B

have hBN : B ≤ N := le_max_right A B

specialize hA N hAN

-- hA : |u N - a| < ε / 2

specialize hB N hBN

-- hB : |u N - b| < ε / 2

rw [abs_lt] at hA hB

-- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2

-- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2

linarith

-- 1ª demostración

-- ===============

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

le_antisymm (aux hb ha) (aux ha hb)

-- Lemas usados

-- ============

-- variable (c d : ℝ)

-- #check (not_le : ¬a ≤ b ↔ b < a)

-- #check (sub_pos : 0 < a - b ↔ b < a)

-- #check (half_pos : a > 0 → a / 2 > 0)

-- #check (le_max_left a b : a ≤ max a b)

-- #check (le_max_right a b : b ≤ max a b)

-- #check (abs_lt : |a| < b ↔ -b < a ∧ a < b)

-- #check (abs_of_pos : 0 < a → |a| = a)

-- #check (add_zero a : a + 0 = a)

-- #check (sub_self a : a - a = 0)

-- #check (abs_add a b : |a + b| ≤ |a| + |b|)

-- #check (abs_sub_comm a b : |a - b| = |b - a|)

-- #check (add_lt_add : a < b → c < d → a + c < b + d)

-- #check (add_halves a : a / 2 + a / 2 = a)

-- #check (lt_irrefl a : ¬a < a)

-- #check (le_antisymm : a ≤ b → b ≤ a → a = b)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory Unicidad_del_limite_de_las_sucesiones_convergentes
imports Main HOL.Real
begin

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

lemma aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed

theorem
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1) by (rule aux)
next
  show "b ≤ a" using assms(1) assms(2) by (rule aux)
qed

end

theory Unicidad_del_limite_de_las_sucesiones_convergentes

imports Main HOL.Real

begin

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

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

lemma aux :

assumes "limite u a"

"limite u b"

shows "b ≤ a"

proof (rule ccontr)

assume "¬ b ≤ a"

let ?ε = "b - a"

have "0 < ?ε/2"

using ‹¬ b ≤ a› by auto

obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"

using assms(1) limite_def ‹0 < ?ε/2› by blast

obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"

using assms(2) limite_def ‹0 < ?ε/2› by blast

let ?C = "max A B"

have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"

using hA by simp

have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"

using hB by simp

have "∀n≥?C. ¦a - b¦ < ?ε"

proof (intro allI impI)

fix n assume "n ≥ ?C"

have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp

also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp

finally show "¦a - b¦ < b - a"

using hCa hCb ‹n ≥ ?C› by fastforce

qed

then show False by fastforce

qed

theorem

assumes "limite u a"

"limite u b"

shows "a = b"

proof (rule antisym)

show "a ≤ b" using assms(2) assms(1) by (rule aux)

show "b ≤ a" using assms(1) assms(2) by (rule aux)

qed

end

Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b

PorJosé A. Alonso 5 febrero 202419 febrero 2024

Demostrar con Lean4 que si la sucesión \(u\) converge a \(a\) y la \(v\) a \(b\), entonces \(u+v\) converge a \(a+b\).

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

import Mathlib.Data.Real.Basic
variable {s t : ℕ → ℝ} {a b c : ℝ}

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
by sorry

import Mathlib.Data.Real.Basic

variable {s t : ℕ → ℝ} {a b c : ℝ}

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

∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

by sorry

La sucesión constante sₙ = c converge a c

PorJosé A. Alonso 2 febrero 202418 febrero 2024

En Lean, una sucesión \(s₀, s₁, s₂, …\) se puede representar mediante una función \(s : ℕ → ℝ\) de forma que \(s(n)\) es \(sₙ\).

Se define que a es el límite de la sucesión \(s\), por

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

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

Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).

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

import Mathlib.Data.Real.Basic

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

example : limite (fun _ : ℕ ↦ c) c :=
by sorry

import Mathlib.Data.Real.Basic

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

∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

example : limite (fun _ : ℕ ↦ c) c :=

by sorry

Suma de potencias de dos

PorJosé A. Alonso 25 septiembre 202124 septiembre 2021

Demostrar que

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

1	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

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

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

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

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

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

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

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

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

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

PorJosé A. Alonso 24 septiembre 202120 septiembre 2021

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

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

1	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

1 2	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)

1	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

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

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

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

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

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