English
If g is strictly concave on a convex set s and f is integrable with values in s, then either f is almost everywhere constant at its average or the average of g∘f is strictly less than g at the average of f.
Русский
Если g строго вогнута на выпуклом множестве s и f интегрируема с значениями в s, тогда либо f почти наверняка равно константе на своем среднем значении, либо среднее значение g(f) strictly меньше g(среднего f).
LaTeX
$$$$ f =^\ae_\mu \text{const}(\alpha, \langle f \rangle_\mu) \lor \langle g(f) \rangle_\mu < g\bigl(\langle f \rangle_\mu\bigr). $$$$
Lean4
/-- **Jensen's inequality**, strict version: if an integrable function `f : α → E` takes values in a
convex closed set `s`, and `g : E → ℝ` is continuous and strictly concave on `s`, then
either `f` is a.e. equal to its average value, or `⨍ x, g (f x) ∂μ < g (⨍ x, f x ∂μ)`. -/
theorem ae_eq_const_or_lt_map_average [IsFiniteMeasure μ] (hg : StrictConcaveOn ℝ s g) (hgc : ContinuousOn g s)
(hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :
f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ (⨍ x, g (f x) ∂μ) < g (⨍ x, f x ∂μ) := by
simpa only [Pi.neg_apply, average_neg, neg_lt_neg_iff] using
hg.neg.ae_eq_const_or_map_average_lt hgc.neg hsc hfs hfi hgi.neg
