theorem chebyshev_inequality {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.MemLp X 2 μ) {a : ℝ} (ha : 0 < a) : μ.real {ω : Ω | a ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ProbabilityTheory.variance X μ / a ^ 2

Chebyshev's inequality. If X has finite mean and variance, then for any a > 0, P{|X − E[X]| ≥ a} ≤ Var(X) / a². The result is derived from Markov's inequality applied to (X − E[X])².