English
If g is concave on a convex closed set s, and μ is a probability measure, and f maps μ-a.e. into s with integrability assumptions, then the average of g∘f is at most g of the average of f.
Русский
Если g выпукло-обратна к x, выпуклое закрытое множество s, μ — вероятностная мера, функция f принимает значения в s почти всюду и интегрируема, то среднее значение g(f) не превосходит g среднего значения f.
LaTeX
$$$\\int g(f) \\, d\\mu \\le g\\left(\\int f \\, d\\mu\\right)$$$
Lean4
/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed
set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points
to `s`, then the expected value of `g ∘ f` is less than or equal to the value of `g` at the expected
value of `f` provided that both `f` and `g ∘ f` are integrable. -/
theorem le_map_integral [IsProbabilityMeasure μ] (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)
(hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :
(∫ x, g (f x) ∂μ) ≤ g (∫ x, f x ∂μ) := by
simpa only [average_eq_integral] using hg.le_map_average hgc hsc hfs hfi hgi
