exists_le_lintegral — Mathlib

English

If f is AEMeasurable, there exists x with f(x) ≤ lavg with respect to μ.

Русский

Если f измерима в среднем почти всюду, то существует x такое, что f(x) не больше среднего значения lavg(f).

LaTeX

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

Lean4

/-- **First moment method**. The minimum of a measurable function is smaller than its integral. -/
theorem exists_le_lintegral (hf : AEMeasurable f μ) : ∃ x, f x ≤ ∫⁻ a, f a ∂μ := by
  simpa only [laverage_eq_lintegral] using exists_le_laverage (IsProbabilityMeasure.ne_zero μ) hf

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