Lemma 3.2 — Chebyshev for sums of independent [0,1] variables: Pr[|X − μ| ≥ α] ≤ μ/α²

Proved

ComplementFreeCA.CFRounding.chebyshev_corollary

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

concentration-inequalitiesp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1probability

Let $X_1,\dots,X_N$ be independent random variables on a probability space, each taking values in $[0,1]$ , let $X=X_1+\dots+X_N$ and $\mu=E[X]$ . Then for every $\alpha>0$ ,

\Pr\big[|X-\mu|\ge\alpha\big]\le\frac{\mu}{\alpha^2}.

The paper uses this corollary of Chebyshev's inequality to show that the welfare of the rounded preallocation is unlikely to fall below a third of its expectation $OPT^*$ .

Formalization Note The variables are real-valued, measurable, independent in the sense of Mathlib's iIndepFun, and take values in $[0,1]$ at every sample point; the number $N$ of variables is arbitrary. Expectation is the Bochner integral, which is the true expectation here because $X$ is bounded and measurable.

Preamble

import Mathlib

Formal statement

namespace ComplementFreeCA.CFRounding

open MeasureTheory ProbabilityTheory

theorem chebyshev_corollary {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] {N : ℕ} (X : Fin N → Ω → ℝ)
    (hmeas : ∀ i, Measurable (X i)) (hind : iIndepFun X μ)
    (hrange : ∀ i ω, X i ω ∈ Set.Icc (0 : ℝ) 1) (α : ℝ) (hα : 0 < α) :
    μ.real {ω | α ≤ |∑ i, X i ω - ∫ ω', ∑ i, X i ω' ∂μ|} ≤ (∫ ω', ∑ i, X i ω' ∂μ) / α ^ 2 := by sorry

end ComplementFreeCA.CFRounding

Source

Dobzinski, Nisan, Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Math. Oper. Res. 35(1), 2010, p. 6, Lemma 3.2

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph