convexOn_log_Gamma — Mathlib

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

Похожие утверждения