measure_le_integral_pos — Mathlib

English

For integrable f with μ a probability measure, there exists x such that the average of f does not exceed f(x) or equivalently the mean is bounded by some value of f.

Русский

Если f интегрируема по вероятностной мере μ, существует x, для которого среднее значение f не превосходит f(x).

LaTeX

$$$\\exists x, \\; \\operatorname{average}_{\\mu} f \\le f(x)$$$

Lean4

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

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