Análisis – Página 8

Teorema del emparedado

PorJosé A. Alonso 18 julio 202118 julio 2021

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 :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

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

1	notation `\|`x`\|` := abs x

Demostrar el teorema del emparedado; es decir, que si para todo n, u(n) ≤ v(n) ≤ w(n) y u(n) tiene el mismo límite que w(n), entonces v(n) también tiene dicho límite.

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

import data.real.basic

variables (u v w : ℕ → ℝ)
variable  (a : ℝ)

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

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

example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
sorry

import data.real.basic

variables (u v w : ℕ → ℝ)

variable (a : ℝ)

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

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

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (u v w : ℕ → ℝ)
variable  (a : ℝ)

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

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

-- Nota. En la demostración se usará el siguiente lema:
lemma max_ge_iff
  {p q r : ℕ}
  : r ≥ max p q ↔ r ≥ p ∧ r ≥ q :=
max_le_iff

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

example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
begin
  intros ε hε,
  cases hu ε hε with N hN, clear hu,
  cases hw ε hε with N' hN', clear hw hε,
  use max N N',
  intros n hn,
  rw max_ge_iff at hn,
  specialize hN n hn.1,
  specialize hN' n hn.2,
  specialize h n,
  specialize h' n,
  clear hn,
  rw abs_le at *,
  split,
  { calc -ε
         ≤ u n - a : hN.1
     ... ≤ v n - a : by linarith, },
  { calc v n - a
         ≤ w n - a : by linarith
     ... ≤ ε       : hN'.2, },
end

-- 2ª demostración
example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
begin
  intros ε hε,
  cases hu ε hε with N hN, clear hu,
  cases hw ε hε with N' hN', clear hw hε,
  use max N N',
  intros n hn,
  rw max_ge_iff at hn,
  specialize hN n (by linarith),
  specialize hN' n (by linarith),
  specialize h n,
  specialize h' n,
  rw abs_le at *,
  split,
  { linarith, },
  { linarith, },
end

-- 3ª demostración
example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
begin
  intros ε hε,
  cases hu ε hε with N hN, clear hu,
  cases hw ε hε with N' hN', clear hw hε,
  use max N N',
  intros n hn,
  rw max_ge_iff at hn,
  specialize hN n (by linarith),
  specialize hN' n (by linarith),
  specialize h n,
  specialize h' n,
  rw abs_le at *,
  split ; linarith,
end

-- 4ª demostración
example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
assume ε,
assume hε : ε > 0,
exists.elim (hu ε hε)
  ( assume N,
    assume hN : ∀ (n : ℕ), n ≥ N → |u n - a| ≤ ε,
    exists.elim (hw ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |w n - a| ≤ ε,
        show ∃ N, ∀ n, n ≥ N → |v n - a| ≤ ε, from
          exists.intro (max N N')
            ( assume n,
              assume hn : n ≥ max N N',
              have h1 : n ≥ N ∧ n ≥ N',
                from max_ge_iff.mp hn,
              have h2 : -ε ≤ v n - a,
                { have h2a : |u n - a| ≤ ε,
                    from hN n h1.1,
                  calc -ε
                       ≤ u n - a : and.left (abs_le.mp h2a)
                   ... ≤ v n - a : by linarith [h n], },
              have h3 : v n - a ≤ ε,
                { have h3a : |w n - a| ≤ ε,
                    from hN' n h1.2,
                  calc v n - a
                       ≤ w n - a : by linarith [h' n]
                   ... ≤ ε       : and.right (abs_le.mp h3a), },
              show |v n - a| ≤ ε,
                from abs_le.mpr (and.intro h2 h3))))

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

import data.real.basic

variables (u v w : ℕ → ℝ)

variable (a : ℝ)

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

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

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- Nota. En la demostración se usará el siguiente lema:

lemma max_ge_iff

{p q r : ℕ}

: r ≥ max p q ↔ r ≥ p ∧ r ≥ q :=

max_le_iff

-- 1ª demostración

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

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

begin

intros ε hε,

cases hu ε hε with N hN, clear hu,

cases hw ε hε with N' hN', clear hw hε,

use max N N',

intros n hn,

rw max_ge_iff at hn,

specialize hN n hn.1,

specialize hN' n hn.2,

specialize h n,

specialize h' n,

clear hn,

rw abs_le at *,

split,

{ calc -ε

≤ u n - a : hN.1

... ≤ v n - a : by linarith, },

{ calc v n - a

≤ w n - a : by linarith

... ≤ ε : hN'.2, },

end

-- 2ª demostración

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

begin

intros ε hε,

cases hu ε hε with N hN, clear hu,

cases hw ε hε with N' hN', clear hw hε,

use max N N',

intros n hn,

rw max_ge_iff at hn,

specialize hN n (by linarith),

specialize hN' n (by linarith),

specialize h n,

specialize h' n,

rw abs_le at *,

split,

{ linarith, },

end

-- 3ª demostración

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

begin

intros ε hε,

cases hu ε hε with N hN, clear hu,

cases hw ε hε with N' hN', clear hw hε,

use max N N',

intros n hn,

rw max_ge_iff at hn,

specialize hN n (by linarith),

specialize hN' n (by linarith),

specialize h n,

specialize h' n,

rw abs_le at *,

split ; linarith,

end

-- 4ª demostración

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

assume ε,

assume hε : ε > 0,

exists.elim (hu ε hε)

( assume N,

assume hN : ∀ (n : ℕ), n ≥ N → |u n - a| ≤ ε,

exists.elim (hw ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |w n - a| ≤ ε,

show ∃ N, ∀ n, n ≥ N → |v n - a| ≤ ε, from

exists.intro (max N N')

( assume n,

assume hn : n ≥ max N N',

have h1 : n ≥ N ∧ n ≥ N',

from max_ge_iff.mp hn,

have h2 : -ε ≤ v n - a,

{ have h2a : |u n - a| ≤ ε,

from hN n h1.1,

calc -ε

≤ u n - a : and.left (abs_le.mp h2a)

... ≤ v n - a : by linarith [h n], },

have h3 : v n - a ≤ ε,

{ have h3a : |w n - a| ≤ ε,

from hN' n h1.2,

calc v n - a

≤ w n - a : by linarith [h' n]

... ≤ ε : and.right (abs_le.mp h3a), },

show |v n - a| ≤ ε,

from abs_le.mpr (and.intro h2 h3))))

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 Teorema_del_emparedado
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"
          "limite w a"
          "∀n. u n ≤ v n"
          "∀n. v n ≤ w n"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume hε : "0 < ε"
  obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"
    using assms(1) hε limite_def
    by auto
  obtain N' where hN' : "∀n≥N'. ¦w n - a¦ < ε"
    using assms(2) hε limite_def
    by auto
  have "∀n≥max N N'. ¦v n - a¦ < ε"
  proof (intro allI impI)
    fix n
    assume hn : "n≥max N N'"
    have "v n - a < ε"
    proof -
      have "v n - a ≤ w n - a"
        using assms(4) by simp
      also have "… ≤ ¦w n - a¦"
        by simp
      also have "… < ε"
        using hN' hn by auto
      finally show "v n - a < ε" .
    qed
    moreover
    have "-(v n - a) < ε"
    proof -
      have "-(v n - a) ≤ -(u n - a)"
        using assms(3) by auto
      also have "… ≤ ¦u n - a¦"
        by simp
      also have "… < ε"
        using hN hn by auto
      finally show "-(v n - a) < ε" .
    qed
    ultimately show "¦v n - a¦ < ε"
      by (simp only: abs_less_iff)
  qed
  then show "∃k. ∀n≥k. ¦v n - a¦ < ε"
    by (rule exI)
qed

end

theory Teorema_del_emparedado

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"

"limite w a"

"∀n. u n ≤ v n"

"∀n. v n ≤ w n"

shows "limite v a"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume hε : "0 < ε"

obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"

using assms(1) hε limite_def

by auto

obtain N' where hN' : "∀n≥N'. ¦w n - a¦ < ε"

using assms(2) hε limite_def

by auto

have "∀n≥max N N'. ¦v n - a¦ < ε"

proof (intro allI impI)

fix n

assume hn : "n≥max N N'"

have "v n - a < ε"

proof -

have "v n - a ≤ w n - a"

using assms(4) by simp

also have "… ≤ ¦w n - a¦"

by simp

also have "… < ε"

using hN' hn by auto

finally show "v n - a < ε" .

qed

moreover

have "-(v n - a) < ε"

proof -

have "-(v n - a) ≤ -(u n - a)"

using assms(3) by auto

also have "… ≤ ¦u n - a¦"

by simp

also have "… < ε"

using hN hn by auto

finally show "-(v n - a) < ε" .

qed

ultimately show "¦v n - a¦ < ε"

by (simp only: abs_less_iff)

qed

then show "∃k. ∀n≥k. ¦v n - a¦ < ε"

by (rule exI)

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]

Producto de sucesiones convergentes a cero

PorJosé A. Alonso 17 julio 202117 julio 2021

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 :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

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

1	notation `\|`x`\|` := abs x

Demostrar que si las sucesiones u(n) y v(n) convergen a cero, entonces u(n)·v(n) también converge a cero.

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

import data.real.basic
import tactic

variables {u v : ℕ → ℝ}
variables {: ℝ}

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

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
sorry

import data.real.basic

import tactic

variables {u v : ℕ → ℝ}

variables {: ℝ}

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

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

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variables {u v : ℕ → ℝ}
variables {: ℝ}

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

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

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
begin
  intros ε hε,
  cases hu ε hε with U hU,
  cases hv 1 zero_lt_one with V hV,
  set N := max U V with hN,
  use N,
  intros n hn,
  specialize hU n (le_of_max_le_left hn),
  specialize hV n (le_of_max_le_right hn),
  rw sub_zero at *,
  calc |(u * v) n|
       = |u n * v n|   : rfl
   ... = |u n| * |v n| : abs_mul (u n) (v n)
   ... < ε * 1         : mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))
   ... = ε             : mul_one ε,
end

-- 2ª demostración
-- ===============

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
begin
  intros ε hε,
  cases hu ε hε with U hU,
  cases hv 1 (by linarith) with V hV,
  set N := max U V with hN,
  use N,
  intros n hn,
  specialize hU n (le_of_max_le_left hn),
  specialize hV n (le_of_max_le_right hn),
  rw sub_zero at *,
  calc |(u * v) n|
       = |u n * v n|   : rfl
   ... = |u n| * |v n| : abs_mul (u n) (v n)
   ... < ε * 1         : by { apply mul_lt_mul'' hU hV ; simp [abs_nonneg] }
   ... = ε             : mul_one ε,
end

-- 3ª demostración
-- ===============

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
begin
  intros ε hε,
  cases hu ε hε with U hU,
  cases hv 1 (by linarith) with V hV,
  set N := max U V with hN,
  use N,
  intros n hn,
  have hUN : U ≤ N := le_max_left U V,
  have hVN : V ≤ N := le_max_right U V,
  specialize hU n (by linarith),
  specialize hV n (by linarith),
  rw sub_zero at ⊢ hU hV,
  rw pi.mul_apply,
  rw abs_mul,
  convert mul_lt_mul'' hU hV _ _, simp,
  all_goals {apply abs_nonneg},
end

import data.real.basic

import tactic

variables {u v : ℕ → ℝ}

variables {: ℝ}

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

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

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

-- 1ª demostración

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

begin

intros ε hε,

cases hu ε hε with U hU,

cases hv 1 zero_lt_one with V hV,

set N := max U V with hN,

use N,

intros n hn,

specialize hU n (le_of_max_le_left hn),

specialize hV n (le_of_max_le_right hn),

rw sub_zero at *,

calc |(u * v) n|

= |u n * v n| : rfl

... = |u n| * |v n| : abs_mul (u n) (v n)

... < ε * 1 : mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))

... = ε : mul_one ε,

end

-- 2ª demostración

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

begin

intros ε hε,

cases hu ε hε with U hU,

cases hv 1 (by linarith) with V hV,

set N := max U V with hN,

use N,

intros n hn,

specialize hU n (le_of_max_le_left hn),

specialize hV n (le_of_max_le_right hn),

rw sub_zero at *,

calc |(u * v) n|

= |u n * v n| : rfl

... = |u n| * |v n| : abs_mul (u n) (v n)

... < ε * 1 : by { apply mul_lt_mul'' hU hV ; simp [abs_nonneg] }

... = ε : mul_one ε,

end

-- 3ª demostración

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

begin

intros ε hε,

cases hu ε hε with U hU,

cases hv 1 (by linarith) with V hV,

set N := max U V with hN,

use N,

intros n hn,

have hUN : U ≤ N := le_max_left U V,

have hVN : V ≤ N := le_max_right U V,

specialize hU n (by linarith),

specialize hV n (by linarith),

rw sub_zero at ⊢ hU hV,

rw pi.mul_apply,

rw abs_mul,

convert mul_lt_mul'' hU hV _ _, simp,

all_goals {apply abs_nonneg},

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 Producto_de_sucesiones_convergentes_a_cero
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 0"
          "limite v 0"
  shows   "limite (λ n. u n * v n) 0"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume  hε : "0 < ε"
  then obtain U where hU : "∀n≥U. ¦u n - 0¦ < ε"
    using assms(1) limite_def
    by auto
  obtain V where hV : "∀n≥V. ¦v n - 0¦ < 1"
    using hε assms(2) limite_def
    by fastforce
  have "∀n≥max U V. ¦u n * v n - 0¦ < ε"
  proof (intro allI impI)
    fix n
    assume hn : "max U V ≤ n"
    then have "U ≤ n"
      by simp
    then have "¦u n - 0¦ < ε"
      using hU by blast
    have hnV : "V ≤ n"
      using hn by simp
    then have "¦v n - 0¦ < 1"
      using hV by blast
    have "¦u n * v n - 0¦ = ¦(u n - 0) * (v n - 0)¦"
      by simp
    also have "… = ¦u n - 0¦ * ¦v n - 0¦"
      by (simp add: abs_mult)
    also have "… < ε * 1"
      using ‹¦u n - 0¦ < ε› ‹¦v n - 0¦ < 1›
      by (rule abs_mult_less)
    also have "… = ε"
      by simp
    finally show "¦u n * v n - 0¦ < ε"
      by this
  qed
  then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"
    by (rule exI)
qed

end

theory Producto_de_sucesiones_convergentes_a_cero

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 0"

"limite v 0"

shows "limite (λ n. u n * v n) 0"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume hε : "0 < ε"

then obtain U where hU : "∀n≥U. ¦u n - 0¦ < ε"

using assms(1) limite_def

by auto

obtain V where hV : "∀n≥V. ¦v n - 0¦ < 1"

using hε assms(2) limite_def

by fastforce

have "∀n≥max U V. ¦u n * v n - 0¦ < ε"

proof (intro allI impI)

fix n

assume hn : "max U V ≤ n"

then have "U ≤ n"

by simp

then have "¦u n - 0¦ < ε"

using hU by blast

have hnV : "V ≤ n"

using hn by simp

then have "¦v n - 0¦ < 1"

using hV by blast

have "¦u n * v n - 0¦ = ¦(u n - 0) * (v n - 0)¦"

by simp

also have "… = ¦u n - 0¦ * ¦v n - 0¦"

by (simp add: abs_mult)

also have "… < ε * 1"

using ‹¦u n - 0¦ < ε› ‹¦v n - 0¦ < 1›

by (rule abs_mult_less)

also have "… = ε"

by simp

finally show "¦u n * v n - 0¦ < ε"

by this

qed

then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"

by (rule exI)

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]

El límite de u(n) es a si y solo si el de u(n)-a es 0

PorJosé A. Alonso 16 julio 20218 julio 2021

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 :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

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

1	notation `\|`x`\|` := abs x

Demostrar que el límite de u(n) es a si y solo si el de u(n)-a es 0.

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

import data.real.basic
import tactic

variable  {u : ℕ → ℝ}
variables {a c x : ℝ}

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

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

example
  : limite u a ↔ limite (λ i, u i - a) 0 :=
sorry

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

variables {a c x : ℝ}

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

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

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

example

: limite u a ↔ limite (λ i, u i - a) 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variable  {u : ℕ → ℝ}
variables {a c x : ℝ}

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

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

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

example
  : limite u a ↔ limite (λ i, u i - a) 0 :=
begin
  split,
  { intros h ε hε,
    convert h ε hε,
    norm_num, },
  { intros h ε hε,
    convert h ε hε,
    norm_num, },
end

-- 2ª demostración
-- ===============

example
  : limite u a ↔ limite (λ i, u i - a) 0 :=
begin
  split;
  { intros h ε hε,
    convert h ε hε,
    norm_num, },
end

-- 3ª demostración
-- ===============

lemma limite_con_suma
  (c : ℝ)
  (h : limite u a)
  : limite (λ i, u i + c) (a + c) :=
λ ε hε, (by convert h ε hε; norm_num)

lemma CNS_limite_con_suma
  (c : ℝ)
  : limite u a ↔ limite (λ i, u i + c) (a + c) :=
begin
  split,
  { apply limite_con_suma },
  { intro h,
    convert limite_con_suma (-c) h; simp, },
end

example
  (u : ℕ → ℝ)
  (a : ℝ)
  : limite u a ↔ limite (λ i, u i - a) 0 :=
begin
  convert CNS_limite_con_suma (-a),
  simp,
end

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

variables {a c x : ℝ}

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

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

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

-- 1ª demostración

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

example

: limite u a ↔ limite (λ i, u i - a) 0 :=

begin

split,

{ intros h ε hε,

convert h ε hε,

norm_num, },

{ intros h ε hε,

convert h ε hε,

norm_num, },

end

-- 2ª demostración

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

example

: limite u a ↔ limite (λ i, u i - a) 0 :=

begin

split;

{ intros h ε hε,

convert h ε hε,

norm_num, },

end

-- 3ª demostración

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

lemma limite_con_suma

(c : ℝ)

(h : limite u a)

: limite (λ i, u i + c) (a + c) :=

λ ε hε, (by convert h ε hε; norm_num)

lemma CNS_limite_con_suma

(c : ℝ)

: limite u a ↔ limite (λ i, u i + c) (a + c) :=

begin

split,

{ apply limite_con_suma },

{ intro h,

convert limite_con_suma (-c) h; simp, },

end

example

(u : ℕ → ℝ)

(a : ℝ)

: limite u a ↔ limite (λ i, u i - a) 0 :=

begin

convert CNS_limite_con_suma (-a),

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 "El_limite_de_u_es_a_syss_el_de_u-a_es_0"
imports Main HOL.Real
begin

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

(* 1ª demostración *)

lemma
  "limite u a ⟷ limite (λ i. u i - a) 0"
proof -
  have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)"
    by (rule limite_def)
  also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"
    by simp
  also have "… ⟷ limite (λ i. u i - a) 0"
    by (rule limite_def[symmetric])
  finally show "limite u a ⟷ limite (λ i. u i - a) 0"
    by this
qed

(* 2ª demostración *)

lemma
  "limite u a ⟷ limite (λ i. u i - a) 0"
proof -
  have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)"
    by (simp only: limite_def)
  also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"
    by simp
  also have "… ⟷ limite (λ i. u i - a) 0"
    by (simp only: limite_def)
  finally show "limite u a ⟷ limite (λ i. u i - a) 0"
    by this
qed

(* 3ª demostración *)

lemma
  "limite u a ⟷ limite (λ i. u i - a) 0"
  using limite_def
  by simp

end

theory "El_limite_de_u_es_a_syss_el_de_u-a_es_0"

imports Main HOL.Real

begin

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

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

(* 1ª demostración *)

lemma

"limite u a ⟷ limite (λ i. u i - a) 0"

proof -

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

by (rule limite_def)

also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"

by simp

also have "… ⟷ limite (λ i. u i - a) 0"

by (rule limite_def[symmetric])

finally show "limite u a ⟷ limite (λ i. u i - a) 0"

by this

qed

(* 2ª demostración *)

lemma

"limite u a ⟷ limite (λ i. u i - a) 0"

proof -

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

by (simp only: limite_def)

also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"

by simp

also have "… ⟷ limite (λ i. u i - a) 0"

by (simp only: limite_def)

finally show "limite u a ⟷ limite (λ i. u i - a) 0"

by this

qed

(* 3ª demostración *)

lemma

"limite u a ⟷ limite (λ i. u i - a) 0"

using limite_def

by simp

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]

Límite multiplicado por una constante

PorJosé A. Alonso 15 julio 20217 julio 2021

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 :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

   notation `|`x`|` := abs 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:

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

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

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

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

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

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 < ε›)

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

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]

Límite de la suma de sucesiones convergentes

PorJosé A. Alonso 14 julio 20216 julio 2021

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 :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

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

1	notation `\|`x`\|` := abs x

Demostrar que el límite de la suma de dos sucesiones convergentes es la suma de los límites de dichas sucesiones.

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

import data.real.basic

variables (u v : ℕ → ℝ)
variables (a b : ℝ)

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

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

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

import data.real.basic

variables (u v : ℕ → ℝ)

variables (a b : ℝ)

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

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

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

example

(hu : limite u a)

(hv : limite v b)

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

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (u v : ℕ → ℝ)
variables (a b : ℝ)

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

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

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  have hε2 : 0 < ε / 2,
    { linarith },
  cases hu (ε / 2) hε2 with Nu hNu,
  cases hv (ε / 2) hε2 with Nv hNv,
  clear hu hv hε2 hε,
  use max Nu Nv,
  intros n hn,
  have hn₁ : n ≥ Nu,
    { exact le_of_max_le_left hn },
  specialize hNu n hn₁,
  have hn₂ : n ≥ Nv,
    { exact le_of_max_le_right hn },
  specialize hNv n hn₂,
  clear hn hn₁ hn₂ Nu Nv,
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|  : by refl
   ... = |(u n - a) + (v n -  b)| : by {congr, ring}
   ... ≤ |u n - a| + |v n -  b|   : by apply abs_add
   ... < ε / 2 + ε / 2            : by linarith
   ... = ε                        : by apply add_halves,
end

-- 2ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  have hn₁ : n ≥ Nu := le_of_max_le_left hn,
  specialize hNu n hn₁,
  have hn₂ : n ≥ Nv := le_of_max_le_right hn,
  specialize hNv n hn₂,
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|  : by refl
   ... = |(u n - a) + (v n -  b)| : by {congr, ring}
   ... ≤ |u n - a| + |v n -  b|   : by apply abs_add
   ... < ε / 2 + ε / 2            : by linarith
   ... = ε                        : by apply add_halves,
end

-- 3ª demostración
-- ===============

lemma max_ge_iff
  {α : Type*}
  [linear_order α]
  {p q r : α}
  : r ≥ max p q  ↔ r ≥ p ∧ r ≥ q :=
max_le_iff

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  cases max_ge_iff.mp hn with hn₁ hn₂,
  have cota₁ : |u n - a| < ε/2 := hNu n hn₁,
  have cota₂ : |v n - b| < ε/2 := hNv n hn₂,
  calc |(u + v) n - (a + b)|
       = |u n + v n - (a + b)|   : by rfl
   ... = |(u n - a) + (v n - b)| : by { congr, ring }
   ... ≤ |u n - a| + |v n - b|   : by apply abs_add
   ... < ε                       : by linarith,
end

-- 4ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  cases max_ge_iff.mp hn with hn₁ hn₂,
  calc |(u + v) n - (a + b)|
       = |u n + v n - (a + b)|   : by refl
   ... = |(u n - a) + (v n - b)| : by { congr, ring }
   ... ≤ |u n - a| + |v n - b|   : by apply abs_add
   ... < ε/2 + ε/2               : add_lt_add (hNu n hn₁) (hNv n hn₂)
   ... = ε                       : by simp
end

-- 5ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  rw max_ge_iff at hn,
  calc |(u + v) n - (a + b)|
       = |u n + v n - (a + b)|   : by refl
   ... = |(u n - a) + (v n - b)| : by { congr, ring }
   ... ≤ |u n - a| + |v n - b|   : by apply abs_add
   ... < ε                       : by linarith [hNu n (by linarith), hNv n (by linarith)],
end

-- 6ª demostración
-- ===============

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε Hε,
  cases hu (ε/2) (by linarith) with L HL,
  cases hv (ε/2) (by linarith) with M HM,
  set N := max L M with hN,
  use N,
  have HLN : N ≥ L := le_max_left _ _,
  have HMN : N ≥ M := le_max_right _ _,
  intros n Hn,
  have H3 : |u n - a| < ε/2 := HL n (by linarith),
  have H4 : |v n - b| < ε/2 := HM n (by linarith),
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|   : by refl
   ... = |(u n - a) + (v n - b)|   : by { congr, ring }
   ... ≤ |(u n - a)| + |(v n - b)| : by apply abs_add
   ... < ε/2 + ε/2                 : by linarith
   ... = ε                         : by ring
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

import data.real.basic

variables (u v : ℕ → ℝ)

variables (a b : ℝ)

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

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

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

-- 1ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

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

begin

intros ε hε,

have hε2 : 0 < ε / 2,

{ linarith },

cases hu (ε / 2) hε2 with Nu hNu,

cases hv (ε / 2) hε2 with Nv hNv,

clear hu hv hε2 hε,

use max Nu Nv,

intros n hn,

have hn₁ : n ≥ Nu,

{ exact le_of_max_le_left hn },

specialize hNu n hn₁,

have hn₂ : n ≥ Nv,

{ exact le_of_max_le_right hn },

specialize hNv n hn₂,

clear hn hn₁ hn₂ Nu Nv,

calc |(u + v) n - (a + b)|

= |(u n + v n) - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by {congr, ring}

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε / 2 + ε / 2 : by linarith

... = ε : by apply add_halves,

end

-- 2ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

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

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

have hn₁ : n ≥ Nu := le_of_max_le_left hn,

specialize hNu n hn₁,

have hn₂ : n ≥ Nv := le_of_max_le_right hn,

specialize hNv n hn₂,

calc |(u + v) n - (a + b)|

= |(u n + v n) - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by {congr, ring}

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε / 2 + ε / 2 : by linarith

... = ε : by apply add_halves,

end

-- 3ª demostración

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

lemma max_ge_iff

{α : Type*}

[linear_order α]

{p q r : α}

: r ≥ max p q ↔ r ≥ p ∧ r ≥ q :=

max_le_iff

example

(hu : limite u a)

(hv : limite v b)

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

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

cases max_ge_iff.mp hn with hn₁ hn₂,

have cota₁ : |u n - a| < ε/2 := hNu n hn₁,

have cota₂ : |v n - b| < ε/2 := hNv n hn₂,

calc |(u + v) n - (a + b)|

= |u n + v n - (a + b)| : by rfl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε : by linarith,

end

-- 4ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

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

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

cases max_ge_iff.mp hn with hn₁ hn₂,

calc |(u + v) n - (a + b)|

= |u n + v n - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε/2 + ε/2 : add_lt_add (hNu n hn₁) (hNv n hn₂)

... = ε : by simp

end

-- 5ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

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

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

rw max_ge_iff at hn,

calc |(u + v) n - (a + b)|

= |u n + v n - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε : by linarith [hNu n (by linarith), hNv n (by linarith)],

end

-- 6ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

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

begin

intros ε Hε,

cases hu (ε/2) (by linarith) with L HL,

cases hv (ε/2) (by linarith) with M HM,

set N := max L M with hN,

use N,

have HLN : N ≥ L := le_max_left _ _,

have HMN : N ≥ M := le_max_right _ _,

intros n Hn,

have H3 : |u n - a| < ε/2 := HL n (by linarith),

have H4 : |v n - b| < ε/2 := HM n (by linarith),

calc |(u + v) n - (a + b)|

= |(u n + v n) - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |(u n - a)| + |(v n - b)| : by apply abs_add

... < ε/2 + ε/2 : by linarith

... = ε : by ring

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 Limite_de_la_suma_de_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¦ < ε)"

(* 1ª demostración *)

lemma
  assumes "limite u a"
          "limite v b"
  shows   "limite (λ n. u n + v n) (a + b)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then have "0 < ε/2"
      by simp
    then have "∃k. ∀n≥k. ¦u n - a¦ < ε/2"
      using assms(1) limite_def by blast
    then obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"
      by (rule exE)
    then have "∃k. ∀n≥k. ¦v n - b¦ < ε/2"
      using ‹0 < ε/2› assms(2) limite_def by blast
    then obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"
      by (rule exE)
    have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"
    proof (intro allI impI)
      fix n :: nat
      assume "n ≥ max Nu Nv"
      have "¦(u n + v n) - (a + b)¦ = ¦(u n - a) + (v n - b)¦"
        by simp
      also have "… ≤ ¦u n - a¦ + ¦v n - b¦"
        by simp
      also have "… < ε/2 + ε/2"
        using hNu hNv ‹max Nu Nv ≤ n› by fastforce
      finally show "¦(u n + v n) - (a + b)¦ < ε"
        by simp
    qed
    then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε "
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "limite u a"
          "limite v b"
  shows   "limite (λ n. u n + v n) (a + b)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then have "0 < ε/2" by simp
    obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"
      using ‹0 < ε/2› assms(1) limite_def by blast
    obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"
      using ‹0 < ε/2› assms(2) limite_def by blast
    have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"
      using hNu hNv
      by (smt (verit, ccfv_threshold) field_sum_of_halves max.boundedE)
    then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε "
      by blast
  qed
qed

end

theory Limite_de_la_suma_de_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¦ < ε)"

(* 1ª demostración *)

lemma

assumes "limite u a"

"limite v b"

shows "limite (λ n. u n + v n) (a + b)"

proof (unfold limite_def)

show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2"

by simp

then have "∃k. ∀n≥k. ¦u n - a¦ < ε/2"

using assms(1) limite_def by blast

then obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"

by (rule exE)

then have "∃k. ∀n≥k. ¦v n - b¦ < ε/2"

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

then obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"

by (rule exE)

have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"

proof (intro allI impI)

fix n :: nat

assume "n ≥ max Nu Nv"

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

by simp

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

by simp

also have "… < ε/2 + ε/2"

using hNu hNv ‹max Nu Nv ≤ n› by fastforce

finally show "¦(u n + v n) - (a + b)¦ < ε"

by simp

qed

then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε "

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "limite u a"

"limite v b"

shows "limite (λ n. u n + v n) (a + b)"

proof (unfold limite_def)

show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2" by simp

obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"

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

obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"

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

have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"

using hNu hNv

by (smt (verit, ccfv_threshold) field_sum_of_halves max.boundedE)

then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε "

by blast

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]