--- Título: En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b) Autor: José A. Alonso --- Demostrar con Lean4 que si \(a\) y \(b\) son números reales tales que \(a \leq b\), entonces \[\log(1+e^a) \leq \log(1+e^b)\] Para ello, completar la siguiente teoría de Lean4: 
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
variable (a b : ℝ)

example
  (h : a ≤ b)
  : log (1 + exp a) ≤ log (1 + exp b) :=
by sorry
Demostración en lenguaje natural [mathjax] Por la monotonía del logaritmo, basta demostrar que \begin{align} &0 < 1 + e^a \tag{1} \\ &1 + e^a \leq 1 + e^b \tag{2} \end{align} La (1), por la suma de positivos, se reduce a \begin{align} &0 < 1 \tag{1.1} \\ &0 < e^a \tag{1.2} \end{align} La (1.1) es una propiedad de los números naturales y la (1.2) de la función exponencial.
La (2), por la monotonía de la suma, se reduce a \[e^a \leq e^b\] que, por la monotonía de la exponencial, se reduce a \[a \leq b\] que es la hipótesis. Demostraciones con Lean4 
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
variable (a b : ℝ)

-- 1ª demostración
example
  (h : a ≤ b)
  : log (1 + exp a) ≤ log (1 + exp b) :=
by
  have h1 : (0 : ℝ) < 1 :=
    zero_lt_one
  have h2 : 0 < exp a :=
    exp_pos a
  have h3 : 0 < 1 + exp a :=
    add_pos h1 h2
  have h4 : exp a ≤ exp b :=
    exp_le_exp.mpr h
  have h5 : 1 + exp a ≤ 1 + exp b :=
    add_le_add_left h4 1
  show log (1 + exp a) ≤ log (1 + exp b)
  exact log_le_log' h3 h5

-- 2ª demostraciṕn
example
  (h : a ≤ b)
  : log (1 + exp a) ≤ log (1 + exp b) :=
by
  apply log_le_log'
  { apply add_pos
    { exact zero_lt_one }
    { exact exp_pos a }}
  { apply add_le_add_left
    exact exp_le_exp.mpr h }
Demostraciones interactivas Se puede interactuar con las demostraciones anteriores en Lean 4 Web. Referencias