Gamma is strictly log convex

Stream: Is there code for X?

[Snir Broshi]

docs#Real.convexOn_log_Gamma and docs#Real.convexOn_Gamma are about convexity.
How can we prove StrictConvexOn rather than ConvexOn? Is there an easy way to get it from the ConvexOn theorem?

The current convexity proof uses Hölder's inequality (docs#MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg) which is a weak inequality, and while Wikipedia does mention some iff condition for equality such a theorem does not exist in Mathlib.

Wikipedia suggests showing $\psi^{(1)}(x) > 0$ since the polygamma function has a series representation where all terms are positive, which then implies $\Gamma''(x)\Gamma(x) > \Gamma'(x)^2$, which implies strict-log-convexity.