average_mem_hypograph — Mathlib

English

If g is convex on s and continuous, then g at the average is no larger than the average of g∘f.

Русский

Если g выпукла на s и непрерывна, то g при среднем значении f не больше среднего значения g∘f.

LaTeX

$$$g(\\langle f \\rangle_{\\mu}) \\le \\langle g\\circ f \\rangle_{\\mu}$$$

Lean4

theorem average_mem_hypograph [IsFiniteMeasure μ] [NeZero μ] (hg : ConcaveOn ℝ 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 ∧ p.2 ≤ g p.1} := by
  simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
    hg.neg.average_mem_epigraph hgc.neg hsc hfs hfi hgi.neg

Похожие утверждения