Menu Close

DAO: La semana en Calculemus (30 de septiembre 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 a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ

Demostrar que si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ.

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

import analysis.special_functions.log.basic
import tactic
open real
variables a b c : 
 
example
  (h : a  b)
  : c - exp b  c - exp a :=
sorry

Soluciones con Lean

import analysis.special_functions.log.basic
import tactic
open real
variables a b c : 
 
-- 1ª demostración
-- ===============
 
example
  (h : a  b)
  : c - exp b  c - exp a :=
begin
   apply sub_le_sub_left _ c,
   exact exp_le_exp.mpr h,
end
 
-- 2ª demostración
-- ===============
 
example
  (h : a  b)
  : c - exp b  c - exp a :=
sub_le_sub_left (exp_le_exp.mpr h) c
 
-- 3ª demostración
-- ===============
 
example
  (h : a  b)
  : c - b  c - a :=
-- by library_search
sub_le_sub_left h c
 
-- 4ª demostración
-- ===============
 
example
  (h : a  b)
  : c - exp b  c - exp a :=
by linarith [exp_le_exp.mpr h]
 
-- 5ª demostración
-- ===============
 
example
  (h : a  b)
  : c - exp b  c - exp a :=
-- by hint
by finish

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

Referencias

2. Si a, b ∈ ℝ, entonces 2ab ≤ a² + b²

Demostrar que si a, b ∈ ℝ, entonces 2ab ≤ a² + b²

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

import data.real.basic
import tactic
 
variables a b : 
 
example : 2*a*b  a^2 + b^2 :=
sorry

Soluciones con Lean

import data.real.basic
import tactic
 
variables a b : 
 
-- 1ª demostración
example : 2*a*b  a^2 + b^2 :=
begin
  have : 0  (a - b)^2 := sq_nonneg (a - b),
  have : 0  a^2 - 2*a*b + b^2, by linarith,
  show 2*a*b  a^2 + b^2, by linarith,
end
 
-- 2ª demostración
example : 2*a*b  a^2 + b^2 :=
begin
  have h : 0  a^2 - 2*a*b + b^2,
  { calc a^2 - 2*a*b + b^2
        = (a - b)^2                   : by ring
    ...  0                           : by apply pow_two_nonneg },
  calc 2*a*b
       = 2*a*b + 0                   : by ring
   ...  2*a*b + (a^2 - 2*a*b + b^2) : add_le_add (le_refl _) h
   ... = a^2 + b^2                   : by ring
end
 
-- 3ª demostración
example : 2*a*b  a^2 + b^2 :=
begin
  have : 0  a^2 - 2*a*b + b^2,
  { calc a^2 - 2*a*b + b^2
         = (a - b)^2       : by ring
     ...  0               : by apply pow_two_nonneg },
  linarith,
end
 
-- 4ª demostración
example : 2*a*b  a^2 + b^2 :=
-- by library_search
two_mul_le_add_sq a b

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

Referencias

3. Si a, b ∈ ℝ, entonces |ab| ≤ (a² + b²)/2

Demostrar que si a, b ∈ ℝ, entonces |ab| ≤ (a² + b²)/2

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

import data.real.basic
import tactic
 
variables a b : 
 
example : abs (a*b)  (a^2 + b^2) / 2 :=
sorry

Soluciones con Lean

import data.real.basic
import tactic
 
variables a b : 
 
-- 1ª demostración
example : abs (a*b)  (a^2 + b^2) / 2 :=
begin
  apply abs_le.mpr,
  split,
  { have h1 : 0  a^2 + 2*a*b + b^2,
      calc 0  (a+b)^2                : by exact pow_two_nonneg (a + b)
         ... = a^2+2*a*b+b^2          : by ring,
    have h2 : -2*(a*b)  a^2 + b^2,
      calc -2*(a*b)
            -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h1
       ... = a^2 + b^2                : by ring,
    show -((a^2 + b^2) / 2)  a*b,      by linarith [h2] },
  { have h3 : 0  a^2 - 2*a*b + b^2,
      calc 0  (a-b)^2                : by exact pow_two_nonneg (a - b)
         ... = a^2-2*a*b+b^2          : by ring,
    have h4 : 2*(a*b)  a^2 + b^2,
      calc 2*(a*b)
            2*(a*b)+(a^2-2*a*b+b^2)  : by exact le_add_of_nonneg_right h3
       ... = a^2 + b^2                : by ring,
    show a * b  (a^2 + b^2)/2,         by linarith [h4] },
end
 
-- 2ª demostración
example : abs (a*b)  (a^2 + b^2) / 2 :=
begin
  apply abs_le.mpr,
  split,
  { have h1 : 0  a^2 + 2*a*b + b^2,
      calc 0  (a+b)^2                : by exact pow_two_nonneg (a + b)
         ... = a^2+2*a*b+b^2          : by ring,
    have h2 : -2*(a*b)  a^2 + b^2,
      calc -2*(a*b)
            -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h1
       ... = a^2 + b^2                : by ring,
    show -((a^2 + b^2) / 2)  a*b,      by linarith [h2] },
  { have h4 : 2*a*b  a^2 + b^2       := two_mul_le_add_sq a b,
    show a * b  (a^2 + b^2)/2,         by linarith [h4] },
end
 
-- 3ª demostración
example : abs (a*b)  (a^2 + b^2) / 2 :=
begin
  apply abs_le.mpr,
  split,
  { have h1 : 0  a^2 + 2*a*b + b^2,
      calc 0  (a+b)^2                : by exact pow_two_nonneg (a + b)
         ... = a^2+2*a*b+b^2          : by ring,
    have h2 : -2*(a*b)  a^2 + b^2,
      calc -2*(a*b)
            -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h1
       ... = a^2 + b^2                : by ring,
    show -((a^2 + b^2) / 2)  a*b,      by linarith [h2] },
  { show a * b  (a^2 + b^2)/2,         by linarith [two_mul_le_add_sq a b] },
end

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

Referencias

4. Si a, b ∈ ℝ, entonces min(a,b) = min(b,a)

Demostrar que si a, b ∈ ℝ, entonces min(a,b) = min(b,a).

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

import data.real.basic
 
variables a b : 
 
example : min a b = min b a :=
sorry

Soluciones con Lean

import data.real.basic
 
variables a b : 
 
-- 1ª demostración
-- ===============
 
example : min a b = min b a :=
begin
  apply le_antisymm,
  { show min a b  min b a,
    apply le_min,
    { apply min_le_right },
    { apply min_le_left }},
  { show min b a  min a b,
    apply le_min,
    { apply min_le_right },
    { apply min_le_left }},
end
 
-- 2ª demostración
-- ===============
 
example : min a b = min b a :=
begin
  have h :  x y : , min x y  min y x,
  { intros x y,
    apply le_min,
    { apply min_le_right },
    { apply min_le_left }},
  apply le_antisymm,
  apply h,
  apply h,
end
 
-- 3ª demostración
-- ===============
 
example : min a b = min b a :=
begin
  have h :  {x y : }, min x y  min y x,
  { intros x y,
    exact le_min (min_le_right x y) (min_le_left x y) },
  exact le_antisymm h h,
end
 
-- 4ª demostración
-- ===============
 
example : min a b = min b a :=
begin
  apply le_antisymm,
  repeat {
    apply le_min,
    apply min_le_right,
    apply min_le_left },
end

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

Referencias

5. Si a, b ∈ ℝ, entonces max(a,b) = max(b,a)

Demostrar que si a, b ∈ ℝ, entonces max(a,b) = max(b,a)

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

import data.real.basic
 
variables a b : 
 
example : max a b = max b a :=
sorry

Soluciones con Lean

import data.real.basic
 
variables a b : 
 
-- 1ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  apply le_antisymm,
  { show max a b  max b a,
    apply max_le,
    { apply le_max_right },
    { apply le_max_left }},
  { show max b a  max a b,
    apply max_le,
    { apply le_max_right },
    { apply le_max_left }},
end
 
-- 2ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  have h :  x y : , max x y  max y x,
  { intros x y,
    apply max_le,
    { apply le_max_right },
    { apply le_max_left }},
  apply le_antisymm,
  apply h,
  apply h,
end
 
-- 3ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  have h :  {x y : }, max x y  max y x,
  { intros x y,
    exact max_le (le_max_right y x) (le_max_left y x),},
  exact le_antisymm h h,
end
 
-- 4ª demostración
-- ===============
 
example : max a b = max b a :=
begin
  apply le_antisymm,
  repeat {
    apply max_le,
    apply le_max_right,
    apply le_max_left },
end

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

Referencias

ForMatUS