ForMatUS: Pruebas en Lean de “Los supremos de las sucesiones no decrecientes son sus límites”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad

Los supremos de las sucesiones no decrecientes son sus límites

usando los estilos declarativo y aplicativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variable (u : ℕ → ℝ)
variable (M : ℝ)

-- ----------------------------------------------------
-- Nota. Se usarán las siguientes notaciones y
-- definiciones estudiadas anteriormente:
-- + |x| = abs x
-- + limite u c :
--      ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε
-- ----------------------------------------------------

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

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

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    no_decreciente : (ℕ → ℝ) → Prop
-- tal que (no_decreciente) expresa que la sucesión u
-- es no decreciente.
-- ----------------------------------------------------

def no_decreciente : (ℕ → ℝ) → Prop
| u := ∀ n m, n ≤ m → u n ≤ u m

-- ----------------------------------------------------
-- Ejercicio 2. Definir la función
--    es_sup_suc : ℝ → (ℕ → ℝ) → Prop
-- tal que (es_sup_suc M u) expresa que M es el supremo
-- de la sucesión u.
-- ----------------------------------------------------

def es_sup_suc : ℝ → (ℕ → ℝ) → Prop
| M u := (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que si M es un supremo de la
-- sucesión no decreciente u, entonces el límite de u
-- es M.
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold es_sup_suc at h,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { -- unfold no_decreciente at h',
    specialize h' n₀ n hn,
    calc -ε
         = (M - ε) - M : by ring
     ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
     ... ≤ u n - M     : sub_le_sub_right h' M },
  { calc u n - M
         ≤ M - M       : sub_le_sub_right (hM₁ n) M
     ... = 0           : sub_self M
     ... ≤ ε           : le_of_lt hε, },
end

-- 2ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  intros ε hε,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { linarith [h' n₀ n hn] },
  { linarith [hM₁ n] },
end

-- 3ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  intros ε hε,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split ; linarith [h' n₀ n hn, hM₁ n],
end

-- 4ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
assume ε,
assume hε : ε > 0,
have hM₁ : ∀ (n : ℕ), u n ≤ M,
  from h.left,
have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),
  from h.right,
exists.elim (hM₂ ε hε)
  ( assume n₀,
    assume hn₀ : u n₀ ≥ M - ε,
    have h1 : ∀ n, n ≥ n₀ → |u n - M| ≤ ε,
      { assume n,
        assume hn : n ≥ n₀,
        have h2 : -ε ≤ u n - M,
          { have h'a : u n₀ ≤ u n,
              from h' n₀ n hn,
            calc -ε
                 = (M - ε) - M : by ring
             ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
             ... ≤ u n - M     : sub_le_sub_right h'a M },
        have h3 : u n - M ≤ ε,
          { calc u n - M
                 ≤ M - M       : sub_le_sub_right (hM₁ n) M
             ... = 0           : sub_self M
             ... ≤ ε           : le_of_lt hε },
        show |u n - M| ≤ ε,
          from abs_le.mpr (and.intro h2 h3) },
    show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,
      from exists.intro n₀ h1)

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

import data.real.basic

variable (u : ℕ → ℝ)

variable (M : ℝ)

-- ----------------------------------------------------

-- Nota. Se usarán las siguientes notaciones y

-- definiciones estudiadas anteriormente:

-- + |x| = abs x

-- + limite u c :

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

-- ----------------------------------------------------

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

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

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

-- ----------------------------------------------------

-- Ejercicio 1. Definir la función

-- no_decreciente : (ℕ → ℝ) → Prop

-- tal que (no_decreciente) expresa que la sucesión u

-- es no decreciente.

-- ----------------------------------------------------

def no_decreciente : (ℕ → ℝ) → Prop

| u := ∀ n m, n ≤ m → u n ≤ u m

-- ----------------------------------------------------

-- Ejercicio 2. Definir la función

-- es_sup_suc : ℝ → (ℕ → ℝ) → Prop

-- tal que (es_sup_suc M u) expresa que M es el supremo

-- de la sucesión u.

-- ----------------------------------------------------

def es_sup_suc : ℝ → (ℕ → ℝ) → Prop

| M u := (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- ----------------------------------------------------

-- Ejercicio 3. Demostrar que si M es un supremo de la

-- sucesión no decreciente u, entonces el límite de u

-- es M.

-- ----------------------------------------------------

-- 1ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

begin

-- unfold limite,

intros ε hε,

-- unfold es_sup_suc at h,

cases h with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split,

{ -- unfold no_decreciente at h',

specialize h' n₀ n hn,

calc -ε

= (M - ε) - M : by ring

... ≤ u n₀ - M : sub_le_sub_right hn₀ M

... ≤ u n - M : sub_le_sub_right h' M },

{ calc u n - M

≤ M - M : sub_le_sub_right (hM₁ n) M

... = 0 : sub_self M

... ≤ ε : le_of_lt hε, },

end

-- 2ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

begin

intros ε hε,

cases h with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split,

{ linarith [h' n₀ n hn] },

{ linarith [hM₁ n] },

end

-- 3ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

begin

intros ε hε,

cases h with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split ; linarith [h' n₀ n hn, hM₁ n],

end

-- 4ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

assume ε,

assume hε : ε > 0,

have hM₁ : ∀ (n : ℕ), u n ≤ M,

from h.left,

have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),

from h.right,

exists.elim (hM₂ ε hε)

( assume n₀,

assume hn₀ : u n₀ ≥ M - ε,

have h1 : ∀ n, n ≥ n₀ → |u n - M| ≤ ε,

{ assume n,

assume hn : n ≥ n₀,

have h2 : -ε ≤ u n - M,

{ have h'a : u n₀ ≤ u n,

from h' n₀ n hn,

calc -ε

= (M - ε) - M : by ring

... ≤ u n₀ - M : sub_le_sub_right hn₀ M

... ≤ u n - M : sub_le_sub_right h'a M },

have h3 : u n - M ≤ ε,

{ calc u n - M

≤ M - M : sub_le_sub_right (hM₁ n) M

... = 0 : sub_self M

... ≤ ε : le_of_lt hε },

show |u n - M| ≤ ε,

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

show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,

from exists.intro n₀ h1)

Se puede imprimir o compartir con