measure_le_laverage_pos — Mathlib

English

Let μ be a nonzero finite measure and f: α → ℝ≥0∞ be measurable. Then the set of points where f does not exceed its laverage has positive μ-measure.

Русский

Пусть μ — ненулевое измерение с конечной мерой, и f: α → ℝ≥0∞ — измерима. Тогда множество точек, где f не превосходит своего среднего значения по μ, имеет положительную меру μ.

LaTeX

$$$0 < \\mu\\{x\\mid f(x) \\le \\operatorname{lavg}_{\\mu}(f)\\}$$$

Lean4

/-- **First moment method**. A measurable function is smaller than its mean on a set of positive
measure. -/
theorem measure_le_laverage_pos (hμ : μ ≠ 0) (hf : AEMeasurable f μ) : 0 < μ {x | f x ≤ ⨍⁻ a, f a ∂μ} := by
  simpa using measure_le_setLAverage_pos (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _) hf.restrict

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