English
A variant of Jensen's inequality for concave function on hypograph: the average of f and g∘f lies in the hypograph.
Русский
Вариант неравенства Дженсена для выпуклой функции на гипографе: средние значения лежат во гипографе.
LaTeX
$$$\\bigl(\\operatorname{average}_{\\mu} f, \\operatorname{average}_{\\mu} (g\\circ f)\\bigr) \\in \\{ (x,y) : 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 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 set_average_mem_hypograph (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, f x ∂μ, ⨍ x in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1} := by
simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
hg.neg.set_average_mem_epigraph hgc.neg hsc h0 ht hfs hfi hgi.neg
