English
Let μ be a finite measure, s a closed convex set, f: α → E with values in s, and g: E → ℝ continuous and strictly convex on s. Then either f is almost everywhere constant equal to its average, or g evaluated at the average is strictly less than the average of g∘f.
Русский
Пусть μ — конечная мера, s — замкнутое выпуклое множество, f: α → E принимает значения в s, и g: E → ℝ непрерывна и строго выпукла на s. Тогда либо f почти наверняка равно постоянной функции равной своему среднему, либо g(среднее f) строго меньше среднего g(f).
LaTeX
$$$$\text{StrictConvexOn}(\mathbb{R}, s, g) \Rightarrow \Big( f =^\ae_\mu \text{const}(\alpha, \langle f \rangle_\mu) \;\lor\; g\bigl(\langle f \rangle_\mu\bigr) < \langle g\circ f \rangle_\mu \Big).$$$$
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 convex on `s`, then
either `f` is a.e. equal to its average value, or `g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ`. -/
theorem ae_eq_const_or_map_average_lt [IsFiniteMeasure μ] (hg : StrictConvexOn ℝ 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 ∂μ) ∨ g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ :=
by
have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s ∧ g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ := fun ht =>
hg.convexOn.set_average_mem_epigraph hgc hsc ht (measure_ne_top _ _) (ae_restrict_of_ae hfs) hfi.integrableOn
hgi.integrableOn
refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_
rintro ⟨t, hm, h₀, h₀', hne⟩
rcases average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' (hfi.prodMk hgi) with ⟨a, b, ha, hb, hab, h_avg⟩
rw [average_pair hfi hgi, average_pair hfi.integrableOn hgi.integrableOn,
average_pair hfi.integrableOn hgi.integrableOn, Prod.smul_mk, Prod.smul_mk, Prod.mk_add_mk, Prod.mk_inj] at h_avg
simp only [Function.comp] at h_avg
rw [← h_avg.1, ← h_avg.2]
calc
g ((a • ⨍ x in t, f x ∂μ) + b • ⨍ x in tᶜ, f x ∂μ) < a * g (⨍ x in t, f x ∂μ) + b * g (⨍ x in tᶜ, f x ∂μ) :=
hg.2 (this h₀).1 (this h₀').1 hne ha hb hab
_ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ :=
by
gcongr
exacts [(this h₀).2, (this h₀').2]
