mul_meas_ge_le_lintegral — Mathlib

English

A shorthand: Markov's inequality for measurable f implies the same estimate without extra conditions if we view it via the reduction to μ.

Русский

Формулировка Маркова без дополнительной меры по аналогии.

LaTeX

$$$$ \text{Markov: } ε \cdot μ{ x | ε ≤ f(x) } ≤ ∫ f dμ. $$$$

Lean4

/-- **Markov's inequality** also known as **Chebyshev's first inequality**. For a version assuming
`AEMeasurable`, see `mul_meas_ge_le_lintegral₀`. -/
theorem mul_meas_ge_le_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) (ε : ℝ≥0∞) : ε * μ {x | ε ≤ f x} ≤ ∫⁻ a, f a ∂μ :=
  mul_meas_ge_le_lintegral₀ hf.aemeasurable ε

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