English
Let μ be a probability measure on α, and g convex on s with continuous restriction, s closed. If f: α → E lands μ-almost everywhere in s, and f and g ∘ f are integrable with respect to μ, then g of the expectation of f is not larger than the expectation of g ∘ f.
Русский
Пусть μ — распределенная по вероятности мера на α, g выпукла на s с непрерывной ограниченной на s, s замкнуто. Если f: α → E принимает значения в s μ-по почти всей мере и f, g ∘ f интегрируемы, то g(∫ f dμ) ≤ ∫ g(f) dμ.
LaTeX
$$$$ g\left( \int x \; f(x) \, d\mu(x) \right) \le \int x \; g(f(x)) \, d\mu(x). $$$$
Lean4
/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed
set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points
to `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected
value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also
`ConvexOn.map_centerMass_le` for a finite sum version of this lemma. -/
theorem map_integral_le [IsProbabilityMeasure μ] (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)
(hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) : g (∫ x, f x ∂μ) ≤ ∫ x, g (f x) ∂μ :=
by simpa only [average_eq_integral] using hg.map_average_le hgc hsc hfs hfi hgi
