exists_setLAverage_le — Mathlib

English

There exists x ∈ s with f(x) ≤ laverage on s for ENNReal-valued f.

Русский

Существует x ∈ s, для которого f(x) ≤ laverage на s для функции f, принимающей значения в ENNReal.

LaTeX

$$$\\exists x \\in s, \\; f(x) \\le \\operatorname{laverage}_{\\mu|_s} f$$$

Lean4

/-- **First moment method**. The maximum of a measurable function is greater than its mean. -/
theorem exists_setLAverage_le (hμ : μ s ≠ 0) (hs : NullMeasurableSet s μ) (hint : ∫⁻ a in s, f a ∂μ ≠ ∞) :
    ∃ x ∈ s, ⨍⁻ a in s, f a ∂μ ≤ f x :=
  let ⟨x, hx, h⟩ := nonempty_of_measure_ne_zero (measure_setLAverage_le_pos hμ hs hint).ne'
  ⟨x, hx, h⟩

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