English
If g is concave on s, the average pair belongs to the hypograph of g; that is, the average of g∘f is no greater than g at the average of f.
Русский
Если g конкавна на s, пара средних принадлежит гипографу g; т. е. среднее g∘f не превосходит g в среднем f.
LaTeX
$$$\\bigl(\\langle f \\rangle_{\\mu}, \\langle g\\circ f \\rangle_{\\mu}\\bigr) \\in \\{ (x,y) : x\\in s \\wedge y \\le g(x) \\}$$$
Lean4
/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave 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 average value of `g ∘ f` is less than or equal to the value of `g`
at the average value of `f` provided that both `f` and `g ∘ f` are integrable. See also
`ConcaveOn.le_map_centerMass` for a finite sum version of this lemma. -/
theorem le_map_average [IsFiniteMeasure μ] [NeZero μ] (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 ∂μ) :=
(hg.average_mem_hypograph hgc hsc hfs hfi hgi).2
