Chebyshev's inequality for the second moment

For any measure μ and any function Y with values in a type with a norm, whose squared norm is integrable, the set where ‖Y‖ is at least c > 0 has measure at most (∫ ‖Y‖²) / c². This is Markov's inequality applied to ‖Y‖². Unlike ProbabilityTheory.meas_ge_le_variance_div_sq, Y is not centered at its mean, so the bound applies directly to a deviation such as the error of an estimator.

Main statements

• TauCeti.meas_ge_le_integral_norm_sq_div_sq: Chebyshev's inequality for the second moment, μ {c ≤ ‖Y‖} ≤ (∫ ‖Y‖²) / c², for any measure and without centering.
• TauCeti.meas_gt_le_div_sq_of_integral_sq_le: the uncentered Chebyshev inequality μ {η < Y} ≤ v / η² for a real Y with ∫ Y² ≤ v.

References

• R. Vershynin, High-Dimensional Probability (2018), §1.2: Chebyshev's inequality.

theorem TauCeti.meas_ge_le_integral_norm_sq_div_sq {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Norm E] {Y : Ω → E} (hY : MeasureTheory.Integrable (fun (ω : Ω) => ‖Y ω‖ ^ 2) μ) {c : ℝ} (hc : 0 < c) : μ {ω : Ω | c ≤ ‖Y ω‖} ≤ ENNReal.ofReal ((∫ (ω : Ω), ‖Y ω‖ ^ 2 ∂μ) / c ^ 2)

Chebyshev's inequality for the second moment. For any measure, if ‖Y‖² is integrable and 0 < c, the set where ‖Y‖ is at least c has measure at most (∫ ‖Y‖²) / c². Unlike ProbabilityTheory.meas_ge_le_variance_div_sq, Y is not centered at its mean.

theorem TauCeti.meas_gt_le_div_sq_of_integral_sq_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} (hY : MeasureTheory.Integrable (fun (ω : Ω) => Y ω ^ 2) μ) {v η : ℝ} (hv : ∫ (ω : Ω), Y ω ^ 2 ∂μ ≤ v) (hη : 0 < η) : μ {ω : Ω | η < Y ω} ≤ ENNReal.ofReal (v / η ^ 2)

The uncentered Chebyshev inequality. If Y² is integrable with ∫ Y² ≤ v and 0 < η, then the set where Y exceeds η has measure at most v / η².