Theorems · Theorem · special functions

Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma

∀ {s t a b : ℝ},
  0 < s → 0 < t → 0 < a → 0 < b → a + b = 1 → Real.Gamma (a * s + b * t) ≤ Real.Gamma s ^ a * Real.Gamma t ^ b

Log-convexity of the Gamma function on the positive reals (stated in multiplicative form), proved using the Hölder inequality applied to Euler's integral.

Defined in

Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Cited by

1 results in Mathlib

Foundations

Depth 282 from the axioms · uses propext, Classical.choice, Quot.sound