Convexity of the cumulant generating function [UPSTREAM]

The cumulant generating function cgf X μ is convex on integrableExpSet X μ, the interval on which the exponential moments are finite. Mathlib has its analyticity and first two derivatives on the interior of that interval (analyticOn_cgf, deriv_cgf, iteratedDeriv_two_cgf), but not its convexity on the whole interval.

Over a finite measure on a finite type, cgf X μ is a log-sum-exp, so this is the convexity of the log-partition function of a log-linear model in its parameter.

Main declarations

• ProbabilityTheory.convexOn_cgf: cgf X μ is convex on integrableExpSet X μ.

Implementation notes

For a + b = 1, the weighted AM–GM inequality applied pointwise to exp (s * X ω) / mgf X μ s and exp (t * X ω) / mgf X μ t and then integrated gives mgf X μ (a * s + b * t) ≤ mgf X μ s ^ a * mgf X μ t ^ b, which is Hölder's inequality for the exponential moments. Taking logarithms gives convexity.

theorem ProbabilityTheory.convexOn_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : ConvexOn ℝ (integrableExpSet X μ) (cgf X μ)

The cumulant generating function is convex on the interval where it is finite.