Menu Close

DAO: La semana en Calculemus (23 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 G es un grupo y a, b ∈ G, entonces (a * b)⁻¹ = b⁻¹ * a⁻¹

Demostrar que si G es un grupo y a, b ∈ G, entonces

(a * b)⁻¹ = b⁻¹ * a⁻¹

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

import algebra.group
variables {G : Type*} [group G]
variables a b : G
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
sorry

Soluciones con Lean

import algebra.group
variables {G : Type*} [group G]
variables a b : G
 
-- 1ª demostración
-- ===============
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply mul_eq_one_iff_inv_eq.mp,
  calc a * b * (b⁻¹ * a⁻¹)
       = ((a * b) * b⁻¹) * a⁻¹ : (mul_assoc _ _ _).symm
   ... = (a * (b * b⁻¹)) * a⁻¹ : congr_arg (* a⁻¹) (mul_assoc a _ _)
   ... = (a * 1) * a⁻¹         : congr_arg2 _ (congr_arg _ (mul_inv_self b)) rfl
   ... = a * a⁻¹               : congr_arg (* a⁻¹) (mul_one a)
   ... = 1                     : mul_inv_self a
end
 
-- 2ª demostración
-- ===============
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply mul_eq_one_iff_inv_eq.mp,
  calc a * b * (b⁻¹ * a⁻¹)
       = ((a * b) * b⁻¹) * a⁻¹ : by simp only [mul_assoc]
   ... = (a * (b * b⁻¹)) * a⁻¹ : by simp only [mul_assoc]
   ... = (a * 1) * a⁻¹         : by simp only [mul_inv_self]
   ... = a * a⁻¹               : by simp only [mul_one]
   ... = 1                     : by simp only [mul_inv_self]
end
 
-- 3ª demostración
-- ===============
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply mul_eq_one_iff_inv_eq.mp,
  calc a * b * (b⁻¹ * a⁻¹)
       = ((a * b) * b⁻¹) * a⁻¹ : by simp [mul_assoc]
   ... = (a * (b * b⁻¹)) * a⁻¹ : by simp
   ... = (a * 1) * a⁻¹         : by simp
   ... = a * a⁻¹               : by simp
   ... = 1                     : by simp,
end
 
-- 4ª demostración
-- ===============
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
-- by library_search
mul_inv_rev a b
 
-- 5ª demostración
-- ===============
 
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by simp

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

Referencias

2. Si a, b, c, d, e ∈ ℝ tales que a ≤ b, b < c, c ≤ d, d < e, entonces a < e

Demostrar que si a, b, c, d, e ∈ ℝ tales que

a ≤ b
b < c
c ≤ d
d < e

entonces

a < e

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

import data.real.basic
 
variables a b c d e : 
 
example
  (h₀ : a  b)
  (h₁ : b < c)
  (h₂ : c  d)
  (h₃ : d < e) :
  a < e :=
sorry

Soluciones con Lean

import data.real.basic
 
variables a b c d e : 
 
-- 1ª demostración
-- ===============
 
example
  (h₀ : a  b)
  (h₁ : b < c)
  (h₂ : c  d)
  (h₃ : d < e) :
  a < e :=
calc a  b : h₀
   ... < c : h₁
   ...  d : h₂
   ... < e : h₃
 
-- 2ª demostración
-- ===============
 
example
  (h₀ : a  b)
  (h₁ : b < c)
  (h₂ : c  d)
  (h₃ : d < e) :
  a < e :=
begin
  apply lt_of_le_of_lt h₀,
  apply lt_trans h₁,
  apply lt_of_le_of_lt h₂,
  exact h₃,
end
 
-- 3ª demostración
-- ===============
 
example
  (h₀ : a  b)
  (h₁ : b < c)
  (h₂ : c  d)
  (h₃ : d < e) :
  a < e :=
by finish
 
-- 4ª demostración
-- ===============
 
example
  (h₀ : a  b)
  (h₁ : b < c)
  (h₂ : c  d)
  (h₃ : d < e) :
  a < e :=
by linarith

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

Referencias

3. Si a, b, d ∈ ℝ tales que 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

Demostrar que si a, b, d ∈ ℝ tales que 1 \leq a y b \leq d, entonces 2 + a + e^b \leq 3a + e^d.

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

import analysis.special_functions.log.basic
open real
variables a b d : 
 
example
  (h  : 1  a)
  (h' : b  d)
  : 2 + a + exp b  3 * a + exp d :=
sorry

Nota: Se pueden usar los lemas

add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d
exp_le_exp : exp a ≤ exp b ↔ a ≤ b

Soluciones con Lean

import analysis.special_functions.log.basic
open real
variables a b d : 
 
-- 1ª demostración
-- ===============
 
example
  (h  : 1  a)
  (h' : b  d)
  : 2 + a + exp b  3 * a + exp d :=
begin
  apply add_le_add,
  { calc 2 + a
         = (1 + 1) + a : by refl
     ...  (1 + a) + a : by simp [h]
     ...  (a + a) + a : by simp [h]
     ... = 3 * a       : by ring },
  { exact exp_le_exp.mpr h', },
end
 
-- 2ª demostración
-- ===============
 
example
  (h  : 1  a)
  (h' : b  d)
  : 2 + a + exp b  3 * a + exp d :=
by linarith [exp_le_exp.mpr h']

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

Referencias

4. Si a, b, c, d, f ∈ ℝ tales que a ≤ b y c < d, entonces a + eᶜ + f < b + eᵈ + f

Demostrar que si a, b, c, d, f ∈ ℝ tales que

a ≤ b
c < d

entonces

a + eᶜ + f < b + eᵈ + f

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

import analysis.special_functions.log.basic
open real
variables a b c d f : 
 
example
  (hab : a  b)
  (hcd : c < d)
  : a + exp c + f < b + exp d + f :=
sorry

Soluciones con Lean

import analysis.special_functions.log.basic
open real
variables a b c d f : 
 
-- 1ª demostración
-- ===============
 
example
  (hab : a  b)
  (hcd : c < d)
  : a + exp c + f < b + exp d + f :=
begin
  apply add_lt_add_of_lt_of_le,
  { apply add_lt_add_of_le_of_lt,
    { exact hab, },
    { apply exp_lt_exp.mpr,
      exact hcd, }},
  { apply le_refl, },
end
 
-- 3ª demostración
-- ===============
 
example
  (hab : a  b)
  (hcd : c < d)
  : a + exp c + f < b + exp d + f :=
begin
  apply add_lt_add_of_lt_of_le,
  { apply add_lt_add_of_le_of_lt hab (exp_lt_exp.mpr hcd), },
  { refl, },
end
 
-- 4ª demostración
-- ===============
 
example
  (hab : a  b)
  (hcd : c < d)
  : a + exp c + f < b + exp d + f :=
add_lt_add_of_lt_of_le
  (add_lt_add_of_le_of_lt hab (exp_lt_exp.mpr hcd))
  (le_refl f)
 
-- 5ª demostración
-- ===============
 
example
  (hab : a  b)
  (hcd : c < d)
  : a + exp c + f < b + exp d + f :=
by linarith [exp_lt_exp.mpr hcd]

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

Referencias

5. Si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ)

Demostrar que si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ).

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

import analysis.special_functions.log.basic
open real
variables a b : 
 
example
  (h : a  b)
  : log (1 + exp a)  log (1 + exp b) :=
sorry

Soluciones con Lean

import analysis.special_functions.log.basic
open real
variables a b : 
 
-- 1ª demostración
-- ===============
 
example
  (h : a  b)
  : log (1 + exp a)  log (1 + exp b) :=
begin
  have h₀ : 0 < 1 + exp a,
  { apply add_pos,
    exact one_pos,
    apply exp_pos, },
  have h₁ : 0 < 1 + exp b,
  { apply add_pos,
    exact one_pos,
    apply exp_pos },
  apply (log_le_log h₀ h₁).mpr,
  apply add_le_add,
   apply le_refl,
  apply exp_le_exp.mpr h,
end
 
-- 2ª demostración
-- ===============
 
example
  (h : a  b)
  : log (1 + exp a)  log (1 + exp b) :=
begin
  have h₀ : 0 < 1 + exp a := add_pos one_pos (exp_pos a),
  have h₁ : 0 < 1 + exp b := add_pos one_pos (exp_pos b),
  exact (log_le_log h₀ h₁).mpr (add_le_add rfl.ge (exp_le_exp.mpr h))
end
 
-- 3ª demostración
-- ===============
 
lemma aux : 0 < 1 + exp a :=
add_pos one_pos (exp_pos a)
 
example
  (h : a  b)
  : log (1 + exp a)  log (1 + exp b) :=
begin
  have h₀ : 0 < 1 + exp a := aux a,
  have h₁ : 0 < 1 + exp b := aux b,
  exact (log_le_log h₀ h₁).mpr (add_le_add rfl.ge (exp_le_exp.mpr h))
end
 
-- 4ª demostración
-- ===============
 
example
  (h : a  b)
  : log (1 + exp a)  log (1 + exp b) :=
(log_le_log (aux a) (aux b)).mpr (add_le_add rfl.ge (exp_le_exp.mpr h))

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

Referencias

ForMatUS