zetesis-puremath Blueprint

4.1 Bounded random variables + concentration

Definition 4.1 Bounded random variable

Lean: ProbabilityTheory.BoundedRandomVariable

\(f : \Omega \to \mathbb {R}\) is bounded in \([a, b]\) under \(\mu \) iff \(f\) is measurable and \(f(\omega ) \in [a, b]\) for \(\mu \)-almost every \(\omega \) [ 5 , § 2.6 ] .

Theorem 4.2 Chebyshev majority bound

Lean: ProbabilityTheory.chebyshev_majority_bound

Let \(X_1, \dots , X_k\) be independent random variables with each \(\mu (A_j) \ge 2/3\) where \(A_j = \{ X_j = \text{correct} \} \). Then for \(k \ge 9 / \delta \), the probability that a majority of the \(X_j\) is correct is at least \(1 - \delta \). Proof via Popoviciu’s variance bound + Chebyshev’s inequality [ 5 , § 2 ] .