theorem ERealFunction.convex_epigraph_iff_jensen_on_dom {H : Type u} [AddCommMonoid H] [Module ℝ H] (f : H → EReal) : Convex ℝ (epigraph f) ↔ ∀ ⦃x y : H⦄, x ∈ dom f → y ∈ dom f → ∀ ⦃α : ℝ⦄, 0 < α → α < 1 → f (α • x + (1 - α) • y) ≤ ↑α * f x + ↑(1 - α) * f y

Proposition 8.4: the real-height epigraph of an extended-real-valued function is convex if and only if Jensen's inequality holds for every two points of the effective domain dom f = {x | f x < ⊤} and every coefficient α ∈ ]0,1[.