theorem jensen_inequality {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX_int : MeasureTheory.Integrable X μ) {φ : ℝ → ℝ} (hφ_convex : ConvexOn ℝ Set.univ φ) (hφX_int : MeasureTheory.Integrable (φ ∘ X) μ) : φ (∫ (ω : Ω), X ω ∂μ) ≤ ∫ (ω : Ω), φ (X ω) ∂μ

Jensen's inequality. If μ is a probability measure on Ω, X : Ω → ℝ is integrable, and φ : ℝ → ℝ is convex (and φ ∘ X is integrable), then φ (∫ X dμ) ≤ ∫ φ(X) dμ. In particular, for a random variable X with finite mean, φ(𝔼 X) ≤ 𝔼 φ(X).