measure_lintegral_le_pos — Mathlib

English

For a probability measure μ and a measurable f: α → ENNReal, there exists x with lintegral μ f ≤ f(x).

Русский

Пусть μ — вероятностное измерение и f: α → ENNReal измерима. Тогда существует x, для которого линеграл ≤ f(x).

LaTeX

$$$\\exists x\\, (\\operatorname{lintegral}_{μ} f) \\le f(x)$$$

Lean4

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

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