English
The function log on the positive real numbers is strictly concave.
Русский
Функция логарифм на положительных вещественных числах строго вогнута.
LaTeX
$$$\text{StrictConcaveOn } \mathbb{R}\ (\mathrm{Ioi}(0))\ \log$$$
Lean4
/-- `Real.exp` is strictly convex on the whole real line. -/
theorem strictConvexOn_exp : StrictConvexOn ℝ univ exp :=
by
apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ
rintro x y z - - hxy hyz
trans exp y
· have h1 : 0 < y - x := by linarith
have h2 : x - y < 0 := by linarith
rw [div_lt_iff₀ h1]
calc
exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
_ = exp y * (1 - exp (x - y)) := by ring
_ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp h2.ne]
_ = exp y * (y - x) := by ring
· have h1 : 0 < z - y := by linarith
rw [lt_div_iff₀ h1]
calc
exp y * (z - y) < exp y * (exp (z - y) - 1) := by
gcongr _ * ?_
linarith [add_one_lt_exp h1.ne']
_ = exp (z - y) * exp y - exp y := by ring
_ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
