English
If f takes values in a strictly convex closed set s and g is continuous and strictly convex on s, then either f equals its average almost everywhere, or the average of g(f) is strictly greater than g evaluated at the average of f.
Русский
Если f принимает значения в строго выпуклом замкнутом множестве s и g непрерывна и строго выпукла на s, то либо f равно своему среднему значению почти всюду, либо среднее по μ g(f) строго больше g среднего f.
LaTeX
$$$$ g(\langle f \rangle_t) < \langle g \circ f \rangle_t \;\text{or} \; f =^a f_{avg}. $$$$
Lean4
/-- If an integrable function `f : α → E` takes values in a strictly convex closed set `s`, then
either it is a.e. equal to its average value, or its average value belongs to the interior of
`s`. -/
theorem ae_eq_const_or_average_mem_interior [IsFiniteMeasure μ] (hs : StrictConvex ℝ s) (hsc : IsClosed s)
(hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) : f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ (⨍ x, f x ∂μ) ∈ interior s :=
by
have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s := fun ht =>
hs.convex.set_average_mem hsc ht (measure_ne_top _ _) (ae_restrict_of_ae hfs) hfi.integrableOn
refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_
rintro ⟨t, hm, h₀, h₀', hne⟩
exact
hs.openSegment_subset (this h₀) (this h₀') hne (average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' hfi)
