English
The function log Γ is convex on the positive real axis Ioi 0.
Русский
Функция log Γ выпукла на положительной вещественной оси Ioi 0.
LaTeX
$$$$ \text{ConvexOn}(\mathbb{R}, Ioi(0), \log \circ \Gamma). $$$$
Lean4
theorem convexOn_log_Gamma : ConvexOn ℝ (Ioi 0) (log ∘ Gamma) :=
by
refine convexOn_iff_forall_pos.mpr ⟨convex_Ioi _, fun x hx y hy a b ha hb hab => ?_⟩
have : b = 1 - a := by linarith
subst this
simp_rw [Function.comp_apply, smul_eq_mul]
simp only [mem_Ioi] at hx hy
rw [← log_rpow, ← log_rpow, ← log_mul]
· gcongr
exact Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma hx hy ha hb hab
all_goals positivity