measure_laverage_le_pos — Mathlib

English

For ENNReal-valued measurable f and μ s ≠ 0, μ s ≠ ∞, the set where f(x) ≤ laverage is of positive measure.

Русский

Для измеримой функции f, принимающей значения ENNReal, и меры μ с μ(s) ≠ 0, μ(s) ≠ ∞, множество, где f(x) ≤ laverage, имеет положительную меру.

LaTeX

$$$0 < \\mu\\{x \\in s \\mid \\laverage_{μ|_s} f \\le f(x)\\}$$$

Lean4

/-- **First moment method**. A measurable function is greater than its mean on a set of positive
measure. -/
theorem measure_laverage_le_pos (hμ : μ ≠ 0) (hint : ∫⁻ a, f a ∂μ ≠ ∞) : 0 < μ {x | ⨍⁻ a, f a ∂μ ≤ f x} := by
  simpa [hint] using @measure_setLAverage_le_pos _ _ _ _ f (measure_univ_ne_zero.2 hμ) nullMeasurableSet_univ

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