exists_lintegral_le — Mathlib

English

For a nonzero finite measure and an AEMeasurable f, there exists x outside a given null set N such that f(x) is at least the laverage of f.

Русский

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

LaTeX

$$$\\exists x\\,(x \\notin N)\\ ∧\\ \\operatorname{lavg}_{μ}(f) \\le f(x)$$$

Lean4

/-- **First moment method**. The maximum of a measurable function is greater than its integral. -/
theorem exists_lintegral_le (hint : ∫⁻ a, f a ∂μ ≠ ∞) : ∃ x, ∫⁻ a, f a ∂μ ≤ f x := by
  simpa only [laverage_eq_lintegral] using exists_laverage_le (IsProbabilityMeasure.ne_zero μ) hint

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