English
More general Jensen-type inequality: average of f and g∘f lies in the epigraph of g over s.
Русский
Обобщение: среднее f и среднего g∘f лежат в эпиграфе g над s.
LaTeX
$$$\\bigl(\\operatorname{average}_{\\mu} f, \\operatorname{average}_{\\mu} (g\\circ f)\\bigr) \\in \\{ (x,y) : x\\in s \\wedge g(x)\\le y\\}$$$
Lean4
theorem average_mem_epigraph [IsFiniteMeasure μ] [NeZero μ] (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s)
(hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :
(⨍ x, f x ∂μ, ⨍ x, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=
by
have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} := hfs.mono fun x hx => ⟨hx, le_rfl⟩
exact average_pair hfi hgi ▸ hg.convex_epigraph.average_mem (hsc.epigraph hgc) ht_mem (hfi.prodMk hgi)
