measure_integral_le_pos — Mathlib

English

For a nonnegative measurable function f, the left average is nonnegative and there exists x with f(x) ≥ left-average.

Русский

Для неотрицательной измеримой функции f левая средняя неотрицательна, и существует x, для которого f(x) не меньше левой средней.

LaTeX

$$$0 < \\mu\\{x : f(x) \\le \\operatorname{laverage}(f)\\}$$$

Lean4

/-- **First moment method**. An integrable function is greater than its integral on a set of
positive measure. -/
theorem measure_integral_le_pos (hf : Integrable f μ) : 0 < μ {x | ∫ a, f a ∂μ ≤ f x} := by
  simpa only [average_eq_integral] using measure_average_le_pos (IsProbabilityMeasure.ne_zero μ) hf

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