mul_meas_ge_le_lintegral₀ — Mathlib

English

A version of Markov's inequality for f with respect to μ holds for any f, giving ε * μ{ x : ε ≤ f x } ≤ ∫ f dμ.

Русский

Версия не ограничена измеримостью для Markov: ε · μ{x : ε ≤ f(x)} ≤ ∫ f dμ.

LaTeX

$$$$ ε \cdot μ\{x \mid ε \le f(x)\} \le \int f \ dμ, $$$$

Lean4

/-- **Markov's inequality** also known as **Chebyshev's first inequality**. -/
theorem mul_meas_ge_le_lintegral₀ {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (ε : ℝ≥0∞) :
    ε * μ {x | ε ≤ f x} ≤ ∫⁻ a, f a ∂μ := by
  simpa only [lintegral_zero, zero_add] using
    lintegral_add_mul_meas_add_le_le_lintegral (ae_of_all _ fun x => zero_le (f x)) hf ε

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