English
Let X: Ω → ℝ be AEStronglyMeasurable, and c > 0. Then the measure of the event |X − μ[X]| ≥ c is bounded by evariance(X, μ)/c^2, in the ENNReal sense.
Русский
Пусть X — AEStronglyMeasurable, c > 0. Тогда вероятность того, что |X − E[X]| ≥ c, не более evariance(X, μ)/c^2.
LaTeX
$$$\mu\{\omega : c \le |X(\omega) - \mu[X]|\} \le \dfrac{\mathrm{evariance}[X;\, \mu]}{c^{2}}$$$
Lean4
/-- **Chebyshev's inequality** for `ℝ≥0∞`-valued variance. -/
theorem meas_ge_le_evariance_div_sq {X : Ω → ℝ} (hX : AEStronglyMeasurable X μ) {c : ℝ≥0} (hc : c ≠ 0) :
μ {ω | ↑c ≤ |X ω - μ[X]|} ≤ evariance X μ / c ^ 2 :=
by
have A : (c : ℝ≥0∞) ≠ 0 := by rwa [Ne, ENNReal.coe_eq_zero]
have B : AEStronglyMeasurable (fun _ : Ω => μ[X]) μ := aestronglyMeasurable_const
convert meas_ge_le_mul_pow_eLpNorm μ two_ne_zero ENNReal.ofNat_ne_top (hX.sub B) A using 1
· congr
simp only [Pi.sub_apply, ENNReal.coe_le_coe, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe]
· rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top]
simp only [ENNReal.toReal_ofNat, one_div, Pi.sub_apply]
rw [div_eq_mul_inv, ENNReal.inv_pow, mul_comm, ENNReal.rpow_two]
congr
simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two, ENNReal.rpow_one,
evariance]
