Uniform i.i.d. coin-flip sample space

Definition

Komlos_RandomSignModel

by xbgxjack · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrepancyprobabilityspencer

The finite i.i.d. fair-coin probability model used to build random $\pm1$ colourings in discrepancy theory. SpOmega n is the sample space of $n$ independent fair coin flips, modelled as Fin n \to \mathrm{Bool}$. spMeasure nis the corresponding product probability measure: the uniform measure onSpOmega n, obtained as the finite product of $n$ copies of the uniform measure on Bool. Each of the $2^n$ outcomes therefore has equal probability $1/2^n$ under spMeasure n`.

This is the standard sample space for the probabilistic method applied to matrix/set-system discrepancy: coordinate j of a draw from spMeasure n gives an independent fair coin used to build a random sign $\varepsilon_j \in \{\pm1\}$ , and sub-Gaussian concentration inequalities (e.g. Hoeffding's inequality) on spMeasure n are the basic tool behind results such as the union-bound colouring in Spencer's entropy method.

Definition code

import Mathlib

namespace Komlos

noncomputable section

/-- The finite sample space of `n` independent fair coin flips, one per coordinate. -/
abbrev SpOmega (n : ℕ) := Fin n → Bool

/-- The uniform (i.i.d. fair-coin) probability measure on `SpOmega n`. -/
def spMeasure (n : ℕ) : MeasureTheory.Measure (SpOmega n) :=
  MeasureTheory.Measure.pi (fun _ : Fin n => (PMF.uniformOfFintype Bool).toMeasure)

instance (n : ℕ) : MeasureTheory.IsProbabilityMeasure (spMeasure n) := by
  unfold spMeasure; infer_instance

end

end Komlos

Source

Standard construction; the finite i.i.d. Bernoulli(1/2) product measure used throughout the probabilistic method in combinatorics, e.g. N. Alon, J. Spencer, The Probabilistic Method, Ch. 1, and as used for the random-colouring step in J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985) 679-706.

View graph