Menu Close

DAO: La semana en Calculemus (4 de noviembre de 2022)

Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:

A continuación se muestran las soluciones.

1. Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0

Demostrar que si X es un espacio métrico y x, y ∈ X, entonces

   0 ≤ dist x y

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

import topology.metric_space.basic
 
variables {X : Type*} [metric_space X]
variables x y : X
 
example : 0  dist x y :=
sorry

Soluciones con Lean

import topology.metric_space.basic
 
variables {X : Type*} [metric_space X]
variables x y : X
 
-- 1ª demostración
example : 0  dist x y :=
  have h1 : 2 * dist x y  0, by calc
    2 * dist x y = dist x y + dist x y : two_mul (dist x y)
             ... = dist x y + dist y x : by rw [dist_comm x y]
             ...  dist x x            : dist_triangle x y x
             ... = 0                   : dist_self x,
  show 0  dist x y,
    by exact nonneg_of_mul_nonneg_left h1 zero_lt_two
 
-- 2ª demostración
example : 0  dist x y :=
-- by library_search
dist_nonneg

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

Referencias

2. Si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε

Demostrar que si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε.

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

import data.real.basic tactic
 
example :
   {x y ε : }, 0 < ε  ε  1  |x| < ε  |y| < ε  |x * y| < ε :=
sorry

Soluciones con Lean

import data.real.basic tactic
 
-- 1ª demostración
-- ===============
 
example :
   {x y ε : }, 0 < ε  ε  1  |x| < ε  |y| < ε  |x * y| < ε :=
begin
  intros x y ε he1 he2 hx hy,
  by_cases h : (|x| = 0),
  { calc |x * y|
         = |x| * |y| : abs_mul x y
     ... = 0 * |y|   : by rw h
     ... = 0         : zero_mul (abs y)
     ... < ε         : he1 },
  { have h1 : 0 < |x|,
    { have h2 : 0  |x| := abs_nonneg x,
      show 0 < |x|,
        exact lt_of_le_of_ne h2 (ne.symm h) },
    calc |x * y|
         = |x| * |y| : abs_mul x y
     ... < |x| * ε   : (mul_lt_mul_left h1).mpr hy
     ... < ε * ε     : (mul_lt_mul_right he1).mpr hx
     ...  1 * ε     : (mul_le_mul_right he1).mpr he2
     ... = ε         : one_mul ε },
end
 
-- 2ª demostración
-- ===============
 
example :
   {x y ε : }, 0 < ε  ε  1  |x| < ε  |y| < ε  |x * y| < ε :=
begin
  intros x y ε he1 he2 hx hy,
  by_cases h : (|x| = 0),
  { calc |x * y|
         = |x| * |y| : by apply abs_mul
     ... = 0 * |y|   : by rw h
     ... = 0         : by apply zero_mul
     ... < ε         : by apply he1 },
  { have h1 : 0 < |x|,
      { have h2 : 0  |x|,
          apply abs_nonneg,
        exact lt_of_le_of_ne h2 (ne.symm h) },
    calc |x * y|
         = |x| * |y| : by rw abs_mul
     ... < |x| * ε   : by apply (mul_lt_mul_left h1).mpr hy
     ... < ε * ε     : by apply (mul_lt_mul_right he1).mpr hx
     ...  1 * ε     : by apply (mul_le_mul_right he1).mpr he2
     ... = ε         : by rw [one_mul] },
end
 
-- 3ª demostración
-- ===============
 
example :
   {x y ε : }, 0 < ε  ε  1  |x| < ε  |y| < ε  |x * y| < ε :=
begin
  intros x y ε he1 he2 hx hy,
  by_cases (|x| = 0),
  { by finish },
  { have : 0 < |x|, by finish,
    calc |x * y|
         = |x| * |y| : by rw abs_mul
     ... < |x| * ε   : by finish
     ...  1 * ε     : by nlinarith
     ... = ε         : by finish },
end

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

Referencias

3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g

Demostrar que la suma de una cota superior de f y una cota superior de g es una cota superior de f+g.

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

import data.real.basic
 
-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f :   ) (a : ) : Prop :=
 x, f x  a
 
variables (f g :   )
variables (a b : )
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
sorry

Soluciones con Lean

import data.real.basic
 
-- (cota_superior f a) se verifica si a es una cota superior de f.
def cota_superior (f :   ) (a : ) : Prop :=
 x, f x  a
 
variables (f g :   )
variables (a b : )
 
-- 1ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
begin
  have h1 :  x, f x + g x  a + b,
  { intro x,
    have h1a : f x  a := hfa x,
    have h1b : g x  b := hgb x,
    show f x + g x  a + b,
      by exact add_le_add (hfa x) (hgb x), },
  show cota_superior (λ x, f x + g x) (a + b),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
begin
  intro x,
  dsimp,
  change f x + g x  a + b,
  apply add_le_add,
  apply hfa,
  apply hgb
end
 
-- 3ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  : cota_superior (λ x, f x + g x) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

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

Referencias

4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g

Demostrar que la suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g.

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

import data.real.basic
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f :   ) (a : ) : Prop :=
 x, a  f x
 
variables (f g :   )
variables (a b : )
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
sorry

Soluciones con Lean

import data.real.basic
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f :   ) (a : ) : Prop :=
 x, a  f x
 
variables (f g :   )
variables (a b : )
 
-- 1ª demostración
-- ===============
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
begin
  have h1 :  x, a + b  f x + g x,
  { intro x,
    have h1a : a  f x := hfa x,
    have h1b : b  g x := hgb x,
    show a + b  f x + g x,
      by exact add_le_add (hfa x) (hgb x), },
  show cota_inferior (λ x, f x + g x) (a + b),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
begin
  intro x,
  dsimp,
  change a + b  f x + g x,
  apply add_le_add,
  apply hfa,
  apply hgb
end
 
-- 3ª demostración
-- ===============
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
λ x, add_le_add (hfa x) (hgb x)

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

Referencias

5. El producto de dos funciones no negativas es no negativa

Demostrar que el producto de dos funciones no negativas es no negativa.

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

import data.real.basic
variables (f g :   )
 
def no_negativa (f :   ) : Prop :=  x, 0  f x
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
sorry

Soluciones con Lean

import data.real.basic
variables (f g :   )
 
def no_negativa (f :   ) : Prop :=  x, 0  f x
 
-- 1ª demostración
-- ===============
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
begin
  have h1 : x, 0  f x * g x,
  { intro x,
    have h2: 0  f x := nnf x,
    have h3: 0  g x := nng x,
    show 0  f x * g x,
      by exact mul_nonneg (nnf x) (nng x), },
  show no_negativa (f * g),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
begin
  intro x,
  change 0  f x * g x,
  apply mul_nonneg,
  apply nnf,
  apply nng
end
 
-- 3ª demostración
-- ===============
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
λ x, mul_nonneg (nnf x) (nng x)

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

Referencias

Posted in ForMatUS