English
Let g be convex on a convex closed set s, and continuous on s. Let μ be a finite, nonzero measure on α, and f: α → E such that f(·) almost everywhere lies in s on a measurable set t with 0 < μ(t) < ∞. If f and g ∘ f are integrable over t with respect to μ, then g evaluated at the average of f over t is at most the average of g(f) over t.
Русский
Пусть g выпукла на выпуклом замкнутом множестве s и непрерывна на s. Пусть μ — конечная, не нулевая мера на α, и f: α → E такова, что μ-пределенная часть множества t удовлетворяет f(x) ∈ s. Если f и g ∘ f интегрируемы на t, то значение g в среднем значении f по t не превосходит среднего значения g(f) по t.
LaTeX
$$$$ g(\langle f \rangle_t) \le \langle g \circ f \rangle_t \;,$$$$
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 of a set `t` to `s`, then the value of `g` at the average value of `f` over `t` is
less than or equal to the average value of `g ∘ f` over `t` provided that both `f` and `g ∘ f` are
integrable. -/
theorem map_set_average_le (hg : ConvexOn ℝ 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 μ) :
g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ :=
(hg.set_average_mem_epigraph hgc hsc h0 ht hfs hfi hgi).2
