English
Let g be concave on a convex closed set s and continuous on s. With a finite, nonzero measure μ on α and a function f: α → E whose μ-a.e. values on t lie in s, if f and g ∘ f are integrable, then the average of g ∘ f over t is at most g evaluated at the average of f over t.
Русский
Пусть g കീ конкавна на выпуклом замкнутом множестве s и непрерывна. Пусть μ — конечная ненулевая мера на α, и f: α → E такова, что μ-ae значения на t лежат в s, и f, g ∘ f интегрируемы. Тогда среднее значение g(f) по t не превосходит g от среднего значения f по t.
LaTeX
$$$$ \langle g \circ f \rangle_t \le g(\langle f \rangle_t) $$$$
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 of a set `t` to `s`, then the average value of `g ∘ f` over `t` is less than or
equal to the value of `g` at the average value of `f` over `t` provided that both `f` and `g ∘ f`
are integrable. -/
theorem le_map_set_average (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s) (h0 : μ t ≠ 0)
(ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s) (hfi : IntegrableOn f t μ) (hgi : IntegrableOn (g ∘ f) t μ) :
(⨍ x in t, g (f x) ∂μ) ≤ g (⨍ x in t, f x ∂μ) :=
(hg.set_average_mem_hypograph hgc hsc h0 ht hfs hfi hgi).2
