English
Under the usual assumptions, the function value at the average is contained in s.
Русский
При обычных предпосылках значение функции в среднем лежит в s.
LaTeX
$$$g(\\langle f \\rangle_{\\mu}) \\le \\langle g\\circ f \\rangle_{\\mu}$$$
Lean4
/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to
the average value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also
`ConvexOn.map_centerMass_le` for a finite sum version of this lemma. -/
theorem map_average_le [IsFiniteMeasure μ] [NeZero μ] (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)
(hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) : g (⨍ x, f x ∂μ) ≤ ⨍ x, g (f x) ∂μ :=
(hg.average_mem_epigraph hgc hsc hfs hfi hgi).2
