Menu Close

Etiqueta: L.ring_nf

Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

José A. Alonso-

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

Para extraer una subsucesión se aplica una función de extracción queconserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

que a es un límite de u por

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

que a es un punto de acumulación de u por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

que la sucesión u es de Cauchy por

   def suc_cauchy (u : ℕ → ℝ) :=
     ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

Demostrar que si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u.

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

import data.real.basic
open nat
 
variable  {u : ℕ → ℝ}
variables {a : ℝ}
variable  {φ : ℕ → ℕ}
 
notation `|`x`|` := abs x
 
def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m
 
def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
 
def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a
 
def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε
 
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable  {u : ℕ → ℝ}
variables {a : ℝ}
variable  {φ : ℕ → ℕ}
 
notation `|`x`|` := abs x
 
def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m
 
def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
 
def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a
 
def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε
 
lemma aux1
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
lemma aux2
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
λ N N', ⟨max N N', ⟨le_max_right N N',
                    le_trans (le_max_left N N')
                             (aux1 h (max N N'))⟩⟩
 
lemma cerca_acumulacion
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end
 
-- 1ª demostración
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold limite,
  intros ε hε,
  unfold suc_cauchy at hu,
  cases hu (ε/2) (half_pos hε) with N hN,
  use N,
  have ha' : ∃ N' ≥ N, |u N' - a| < ε/2,
    apply cerca_acumulacion ha (ε/2) (half_pos hε),
  cases ha' with N' h,
  cases h with hNN' hN',
  intros n hn,
  calc   |u n - a|
       = |(u n - u N') + (u N' - a)| : by ring_nf
   ... ≤ |u n - u N'| + |u N' - a|   : abs_add (u n - u N') (u N' - a)
   ... < ε/2 + |u N' - a|            : add_lt_add_right (hN n hn N' hNN') _
   ... < ε/2 + ε/2                   : add_lt_add_left hN' (ε / 2)
   ... = ε                           : add_halves ε
end
 
-- 2ª demostración
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with N hN,
  use N,
  have ha' : ∃ N' ≥ N, |u N' - a| < ε/2,
    apply cerca_acumulacion ha (ε/2) (by linarith),
  rcases ha' with ⟨N', hNN', hN'⟩,
  intros n hn,
  calc  |u n - a|
      = |(u n - u N') + (u N' - a)| : by ring_nf
  ... ≤ |u n - u N'| + |u N' - a|   : by simp [abs_add]
  ... < ε                           : by linarith [hN n hn N' hNN'],
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

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

Soluciones con Isabelle/HOL
theory "Si_a_es_un_punto_de_acumulacion_de_la_sucesion_de_Cauchy_u,_entonces_a_es_el_limite_de_u"
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"
 
definition suc_cauchy :: "(nat ⇒ real) ⇒ bool"
  where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"
 
(* Lemas auxiliares *)
 
lemma aux1 :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
lemma aux2 :
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  have "max N N' ≥ N' ∧ φ (max N N') ≥ N"
    by (meson assms aux1 max.bounded_iff max.cobounded2)
  then show "∃k ≥ N'. φ k ≥ N"
    by blast
qed
 
lemma cerca_acumulacion :
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where hφ1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using hφ2 limite_def ‹ε > 0› by auto
  obtain m where "m ≥ N' ∧ φ m ≥ N"
    using aux2 hφ1 by blast
  then show "∃k≥N. ¦u k - a¦ < ε"
    using hN' by auto
qed
 
(* Demostración *)
lemma
  assumes "suc_cauchy u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then have "ε/2 > 0"
    by simp
  then obtain N where hN : "∀m≥N. ∀n≥N. ¦u m - u n¦ < ε/2"
    using assms(1) suc_cauchy_def
    by blast
  have "∀k≥N. ¦u k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume hk : "k ≥ N"
    obtain N' where hN'1 : "N' ≥ N" and
                    hN'2 : "¦u N' - a¦ < ε/2"
      using assms(2) cerca_acumulacion ‹ε/2 > 0› by blast
    have "¦u k - a¦ = ¦(u k - u N') + (u N'  - a)¦"
      by simp
    also have "… ≤ ¦u k - u N'¦ + ¦u N'  - a¦"
      by simp
    also have "… < ε/2 + ¦u N'  - a¦"
      using hk hN hN'1 by auto
    also have "… < ε/2 + ε/2"
      using hN'2 by auto
    also have "… = ε"
      by simp
    finally show "¦u k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦u k - a¦ < ε"
    by auto
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>

Soluciones →

La suma de los n primeros impares es n^2

José A. Alonso-

En Lean, se puede definir el n-ésimo número primo por

   def impar (n : ℕ) := 2 * n + 1

Además, en la librería finset están definidas las funciones

   range :: ℕ → finset ℕ
   sum :: finset α → (α → β) → β

tales que

+ (range n) es el conjunto de los n primeros números naturales. Por ejemplo, el valor de (range 3) es {0, 1, 2}.
+ (sum A f) es la suma del conjunto obtenido aplicando la función f a los elementos del conjunto finito A. Por ejemplo, el valor de (sum (range 3) impar) es 9.

Demostrar que la suma de los n primeros números impares es n².

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

import data.finset
import tactic.ring
open nat
 
variable (n : ℕ)
 
def impar (n : ℕ) := 2 * n + 1
 
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
sorry
Soluciones con Lean
import data.finset
import tactic.ring
open nat
 
set_option pp.structure_projections false
 
variable (n : ℕ)
 
def impar (n : ℕ) := 2 * n + 1
 
-- 1ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with m HI,
  { calc finset.sum (finset.range 0) impar
          = 0
            : by simp
     ...  = 0 ^ 2
            : rfl, },
  { calc finset.sum (finset.range (succ m)) impar
         = finset.sum (finset.range m) impar + impar m
           : finset.sum_range_succ impar m
     ... = m ^ 2 + impar m
           : congr_arg2 (+) HI rfl
     ... = m ^ 2 + 2 * m + 1
           : rfl
     ... = (m + 1) ^ 2
           : by ring_nf
     ... = succ m ^ 2
           : rfl },
end
 
-- 2ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with d hd,
  { refl, },
  { rw finset.sum_range_succ,
    rw hd,
    change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2,
    ring_nf, },
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

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

Soluciones con Isabelle/HOL
theory "La_suma_de_los_n_primeros_impares_es_n^2"
imports Main
begin
 
definition impar :: "nat ⇒ nat" where
  "impar n ≡ 2 * n + 1"
 
lemma "sum impar {i::nat. i < n} = n⇧2"
proof (induct n)
  show "sum impar {i. i < 0} = 0⇧2"
    by simp
next
  fix n
  assume HI : "sum impar {i. i < n} = n⇧2"
  have "{i. i < Suc n} = {i. i < n} ∪ {n}"
    by auto
  then have "sum impar {i. i < Suc n} =
             sum impar {i. i < n} + impar n"
    by simp
  also have "… = n⇧2 + (2 * n + 1)"
    using HI impar_def by simp
  also have "… = (n + 1)⇧2"
    by algebra
  also have "… = (Suc n)⇧2"
    by simp
  finally show "sum impar {i. i < Suc n} = (Suc n)⇧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>

Soluciones →

Las sucesiones convergentes son sucesiones de Cauchy

José A. Alonso-

Nota: El problema de hoy lo ha escrito Sara Díaz Real y es uno de los que se encuentran en su Trabajo Fin de Máster Formalización en Lean de problemas de las Olimpiadas Internacionales de Matemáticas (IMO). Concretamente, el problema se encuentra en la página 52 junto con la demostración en lenguaje natural.

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

  • el valor absoluto de x por
     notation `|`x`|` := abs x
  • a es un límite de la sucesión u, por
     def limite (u : ℕ → ℝ) (a : ℝ) :=
       ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| ≤ ε
  • la sucesión u es convergente por
     def suc_convergente (u : ℕ → ℝ) :=
       ∃ l, limite u l
  • la sucesión u es de Cauchy por
     def suc_cauchy (u : ℕ → ℝ) :=
       ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

Demostrar que las sucesiones convergentes son de Cauchy.

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

import data.real.basic
 
variable {u : ℕ → ℝ }
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
 
def suc_convergente (u : ℕ → ℝ) :=
  ∃ l, limite u l
 
def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε
 
example
  (h : suc_convergente u)
  : suc_cauchy u :=
sorry
Soluciones con Lean
import data.real.basic
 
variable {u : ℕ → ℝ }
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
 
def suc_convergente (u : ℕ → ℝ) :=
  ∃ l, limite u l
 
def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε
 
-- 1ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  unfold suc_cauchy,
  intros ε hε,
  have hε2 : 0 < ε/2 := half_pos hε,
  cases h with l hl,
  cases hl (ε/2) hε2 with N hN,
  clear hε hl hε2,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : congr_arg2 (+) rfl (abs_sub_comm l (u q))
   ... ≤ ε/2 + ε/2               : add_le_add (hN p hp) (hN q hq)
   ... = ε                       : add_halves ε,
end
 
-- 2ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (half_pos hε) with N hN,
  clear hε hl,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : congr_arg2 (+) rfl (abs_sub_comm l (u q))
   ... ≤ ε/2 + ε/2               : add_le_add (hN p hp) (hN q hq)
   ... = ε                       : add_halves ε,
end
 
-- 3ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (half_pos hε) with N hN,
  clear hε hl,
  use N,
  intros p hp q hq,
  have cota1 : |u p - l| ≤ ε / 2 := hN p hp,
  have cota2 : |u q - l| ≤ ε / 2 := hN q hq,
  clear hN hp hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : by rw abs_sub_comm l (u q)
   ... ≤ ε                       : by linarith,
end
 
-- 4ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (half_pos hε) with N hN,
  clear hε hl,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : by rw abs_sub_comm l (u q)
   ... ≤ ε                       : by linarith [hN p hp, hN q hq],
end
 
-- 5ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (by linarith) with N hN,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : by simp [abs_add]
   ... = |u p - l|  + |u q - l|  : by simp [abs_sub_comm]
   ... ≤ ε                       : by linarith [hN p hp, hN q hq],
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

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

Soluciones con Isabelle/HOL
theory Las_sucesiones_convergentes_son_sucesiones_de_Cauchy
imports Main HOL.Real
begin
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"
 
definition suc_convergente :: "(nat ⇒ real) ⇒ bool"
  where "suc_convergente u ⟷ (∃ l. limite u l)"
 
definition suc_cauchy :: "(nat ⇒ real) ⇒ bool"
  where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"
 
(* 1ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
  proof (intro allI impI)
    fix p q
    assume hp : "p ≥ k" and hq : "q ≥ k"
    then have hp' : "¦u p - a¦ < ε/2"
      using hk by blast
    have hq' : "¦u q - a¦ < ε/2"
      using hk hq by blast
    have "¦u p - u q¦ = ¦(u p - a) + (a - u q)¦"
      by simp
    also have "… ≤ ¦u p - a¦  + ¦a - u q¦"
      by simp
    also have "… = ¦u p - a¦  + ¦u q - a¦"
      by simp
    also have "… < ε/2 + ε/2"
      using hp' hq' by simp
    also have "… = ε"
      by simp
    finally show "¦u p - u q¦ < ε"
      by this
  qed
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (rule exI)
qed
 
(* 2ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
  proof (intro allI impI)
    fix p q
    assume hp : "p ≥ k" and hq : "q ≥ k"
    then have hp' : "¦u p - a¦ < ε/2"
      using hk by blast
    have hq' : "¦u q - a¦ < ε/2"
      using hk hq by blast
    show "¦u p - u q¦ < ε"
      using hp' hq' by argo
  qed
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (rule exI)
qed
 
(* 3ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    using hk by (smt (z3) field_sum_of_halves)
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (rule exI)
qed
 
(* 3ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (smt (z3) field_sum_of_halves)
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>

Soluciones →