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

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

1 2	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']

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

J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 16.

Share this:

Escribe un comentarioCancel reply