meas_ge_le_lintegral_div — Mathlib

English

Let f be a nonnegative measurable function. For any ε ≠ 0, ε ≠ ∞, the measure of the set where ε ≤ f is bounded by the Lintegral of f over μ divided by ε:

Русский

Пусть f неотрицательно измерима. Для любого ε ≠ 0, ε ≠ ∞ выполнено: μ{x | ε ≤ f(x)} ≤ (∫ f dμ) / ε.

LaTeX

$$$AEMeasurable\\ f\\ μ\\;\\to\\; (ε \\neq 0)\\; (ε \\neq ∞)\\;\\Rightarrow\\; μ\\{x\\;|\\; ε \\le f(x)\\} \\le \\dfrac{\\int f\\,dμ}{ε}$$$

Lean4

/-- **Markov's inequality**, also known as **Chebyshev's first inequality**. -/
theorem meas_ge_le_lintegral_div {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) (hε' : ε ≠ ∞) :
    μ {x | ε ≤ f x} ≤ (∫⁻ a, f a ∂μ) / ε :=
  (ENNReal.le_div_iff_mul_le (Or.inl hε) (Or.inl hε')).2 <|
    by
    rw [mul_comm]
    exact mul_meas_ge_le_lintegral₀ hf ε

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