English
Jensen-type result for the epigraph of g on a convex set: the pair of averages lies in the epigraph.
Русский
Неравенство Дженсена для эпиграфа: пара средних лежит в эпиграфе функции g.
LaTeX
$$$\\bigl( \\operatorname{average}_{\\mu|t} f,\\, \\operatorname{average}_{\\mu|t} (g\\circ f) \\bigr) \\in \\{ (x,y)\\in E\\times\\mathbb{R} : x\\in s \\wedge g(x) \\le y\\}$$$
Lean4
/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex set in `E`, and `f` is an integrable
function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `closure s`:
`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma. -/
theorem set_average_mem_closure (hs : Convex ℝ s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s)
(hfi : IntegrableOn f t μ) : (⨍ x in t, f x ∂μ) ∈ closure s :=
hs.closure.set_average_mem isClosed_closure h0 ht (hfs.mono fun _ hx => subset_closure hx) hfi
