English
Various equivalent forms show that variance bounds can be expressed through linear combinations of moments; the exact equivalences can be written using lattice/real-analytic rearrangements.
Русский
Различные эквивалентные формы показывают, что границы дисперсии выражаются через линейные комбинации моментов; точные эквивалентности записываются с помощью решёток/аналитических преобразований.
LaTeX
$$$$\text{(equivalences between variance bounds)}$$$$
Lean4
/-- **Chebyshev's inequality**: one can control the deviation probability of a real random variable
from its expectation in terms of the variance. -/
theorem meas_ge_le_variance_div_sq [IsFiniteMeasure μ] {X : Ω → ℝ} (hX : MemLp X 2 μ) {c : ℝ} (hc : 0 < c) :
μ {ω | c ≤ |X ω - μ[X]|} ≤ ENNReal.ofReal (variance X μ / c ^ 2) :=
by
rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero hc.ne.symm), hX.ofReal_variance_eq]
convert @meas_ge_le_evariance_div_sq _ _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
· simp only [Real.coe_toNNReal', max_le_iff, abs_nonneg, and_true]
· rw [ENNReal.ofReal_pow hc.le]
rfl
