measure_le_lintegral_pos — Mathlib

English

For a probability measure μ on α and a measurable f: α → ENNReal, the set of points where the lintegral is at most f(x) has positive μ-measure.

Русский

Для вероятностного измерения μ на α и измеримой функции f: α → ENNReal множество точек, для которых линегральная среда не превышает f(x), имеет положительную меру μ.

LaTeX

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

Lean4

/-- **First moment method**. A measurable function is smaller than its integral on a set f
positive measure. -/
theorem measure_le_lintegral_pos (hf : AEMeasurable f μ) : 0 < μ {x | f x ≤ ∫⁻ a, f a ∂μ} := by
  simpa only [laverage_eq_lintegral] using measure_le_laverage_pos (IsProbabilityMeasure.ne_zero μ) hf

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