English
A variant of the set-epigraph Jensen inequality for averages over a set t with measurable f.
Русский
Вариант неравенства Дженсена для эпиграфа над множеством t с функцией f.
LaTeX
$$$\\bigl(\\operatorname{average}_{\\mu|t} f, \\operatorname{average}_{\\mu|t} (g\\circ f)\\bigr)\\in \\{ (x,y)\\;|\\; x\\in s \\wedge g(x)\\le y \\}$$$
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 set_average_mem_epigraph (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 μ) :
(⨍ x in t, f x ∂μ, ⨍ x in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=
have := Fact.mk ht.lt_top
have := NeZero.mk h0
hg.average_mem_epigraph hgc hsc hfs hfi hgi
