Menu Close

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

José A. Alonso

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

A continuación se muestran las soluciones.

1. Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g

Demostrar que si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g.

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

import data.real.basic
 
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
 
def no_negativa (f : ℝ → ℝ) : Prop :=
∀ x, 0 ≤ f x
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
sorry

Soluciones con Lean

import data.real.basic
 
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
 
def no_negativa (f : ℝ → ℝ) : Prop :=
∀ x, 0 ≤ f x
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
-- 1ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
begin
  have h1 : ∀ x, f x * g x ≤ a * b,
    { intro x,
      have h2 : f x ≤ a := hfa x,
      have h3 : g x ≤ b := hgb x,
      have h4 : 0 ≤ g x := nng x,
      show f x * g x ≤ a * b,
        by exact mul_le_mul h2 h3 h4 nna, },
  show cota_superior (f * g) (a * b),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
begin
  intro x,
  change f x * g x ≤ a * b,
  apply mul_le_mul,
  apply hfa,
  apply hgb,
  apply nng,
  apply nna
end
 
-- 3ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
begin
  dunfold cota_superior no_negativa at *,
  intro x,
  have h1:= hfa x,
  have h2:= hgb x,
  have h3:= nng x,
  exact mul_le_mul h1 h2 h3 nna,
end
 
-- 4ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
begin
  dunfold cota_superior no_negativa at *,
  intro x,
  specialize hfa x,
  specialize hgb x,
  specialize nng x,
  exact mul_le_mul hfa hgb nng nna,
end
 
-- 5ª demostración
-- ===============
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
λ x, mul_le_mul (hfa x) (hgb x) (nng x) nna

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

Referencias

2. La suma de dos funciones monótonas es monótona

Demostrar que la suma de dos funciones monótonas es monótona.

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

import data.real.basic
 
variables (f g : ℝ → ℝ)
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f + g) :=
sorry

Soluciones con Lean

import data.real.basic
 
variables (f g : ℝ → ℝ)
 
-- 1ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f + g) :=
begin
  have h1 : ∀ a b, a ≤ b → (f + g) a ≤ (f + g ) b,
    { intros a b hab,
      have h2 : f a ≤ f b := mf hab,
      have h3 : g a ≤ g b := mg hab,
      calc (f + g) a
           = f a + g a : rfl
       ... ≤ f b + g b : add_le_add h2 h3
       ... = (f + g) b : rfl, },
  show monotone (f + g),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f + g) :=
begin
  intros a b hab,
  apply add_le_add,
  apply mf hab,
  apply mg hab
end
 
-- 3ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f + g) :=
λ a b hab, add_le_add (mf hab) (mg hab)

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

Referencias

3. Si f es monótona y c ≥ 0, entonces c·f es monótona

Demostrar que si f es monótona y c ≥ 0, entonces c·f es monótona.

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

import data.real.basic
 
variables (f : ℝ → ℝ)
variable  {c : ℝ}
 
example
  (mf : monotone f)
  (nnc : 0 ≤ c)
  : monotone (λ x, c * f x) :=
sorry

Soluciones con Lean

import data.real.basic
 
variables (f : ℝ → ℝ)
variable  {c : ℝ}
 
-- 1ª demostración
-- ===============
 
example
  (mf : monotone f)
  (nnc : 0 ≤ c)
  : monotone (λ x, c * f x) :=
begin
  have h1 : ∀ a b, a ≤ b → (λ x, c * f x) a ≤ (λ x, c * f x) b,
    { intros a b hab,
      have h2 : f a ≤ f b := mf hab,
      have h3 : c * f a ≤ c * f b := mul_le_mul_of_nonneg_left h2 nnc,
      show (λ x, c * f x) a ≤ (λ x, c * f x) b,
        by exact h3, },
  show monotone (λ x, c * f x),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (mf : monotone f)
  (nnc : 0 ≤ c)
  : monotone (λ x, c * f x) :=
begin
  intros a b hab,
  apply mul_le_mul_of_nonneg_left,
  apply mf hab,
  apply nnc
end
 
-- 3ª demostración
-- ===============
 
example (mf : monotone f) (nnc : 0 ≤ c) :
  monotone (λ x, c * f x) :=
λ a b hab, mul_le_mul_of_nonneg_left (mf hab) nnc

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

Referencias

4. La composición de dos funciones monótonas es monótona

Demostrar que la composición de dos funciones monótonas es monótona.

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

import data.real.basic
 
variables (f g : ℝ → ℝ)
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
sorry

Soluciones con Lean

import data.real.basic
 
variables (f g : ℝ → ℝ)
 
-- 1ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
begin
  have h1 : ∀ a b, a ≤ b → (f ∘ g) a ≤ (f ∘ g) b,
    { intros a b hab,
      have h1 : g a ≤ g b := mg hab,
      have h2 : f (g a) ≤ f (g b) := mf h1,
      show (f ∘ g) a ≤ (f ∘ g) b,
        by exact h2, },
  show monotone (f ∘ g),
    by exact h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
begin
  intros a b hab,
  apply mf,
  apply mg,
  apply hab
end
 
-- 3ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
λ a b hab, mf (mg hab)
 
-- 4ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
-- by library_search
monotone.comp mf mg
 
-- 5ª demostración
-- ===============
 
example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
-- by hint
by tauto

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

Referencias

5. La suma de dos funciones pares es par

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x).

Demostrar que la suma de dos funciones pares es par.

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

import data.real.basic
 
variables (f g : ℝ → ℝ)
 
def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x)
 
example
  (hf : par f)
  (hg : par g)
  : par (f + g) :=
sorry

Soluciones con Lean

import data.real.basic
variables (f g : ℝ → ℝ)
 
def par (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x)
 
-- 1ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : par g)
  : par (f + g) :=
begin
  intro x,
  have h1 : f x = f (-x) := hf x,
  have h2 : g x = g (-x) := hg x,
  calc (f + g) x
       = f x + g x       : rfl
   ... = f (-x) + g x    : congr_arg (+ g x) h1
   ... = f (-x) + g (-x) : congr_arg ((+) (f (-x))) h2
   ... = (f + g) (-x)    : rfl
end
 
-- 2ª demostración
-- ===============
 
example
  (hf : par f)
  (hg : par g)
  : par (f + g) :=
begin
  intro x,
  calc (f + g) x
       = f x + g x       : rfl
   ... = f (-x) + g (-x) : by rw [hf, hg]
   ... = (f + g) (-x)    : rfl
end

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

Referencias

Posted in ForMatUS