Theorems · Theorem · probability

ProbabilityTheory.meas_ge_le_variance_div_sq

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ},
  MeasureTheory.MemLp X 2 μ →
    ∀ {c : ℝ}, 0 < c → μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (ProbabilityTheory.variance X μ / c ^ 2)

Chebyshev's inequality: one can control the deviation probability of a real random variable from its expectation in terms of the variance.

Defined in

Mathlib.Probability.Moments.Variance

Cited by

1 results in Mathlib

Foundations

Depth 255 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasure