The i.i.d. coin-flip measure is the uniform measure on its sample space

Proved

spMeasure_eq_uniform

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

combinatoricsmeasure-theoryprobabilityspencer

Let spMeasure n be the i.i.d. fair-coin product measure on SpOmega n = Fin n \to \mathrm{Bool}$ (the finite product of $n$ copies of the uniform measure on $\{\mathrm{true},\mathrm{false}\}$). Then spMeasure ncoincides exactly with the uniform probability measure on the finite typeSpOmega n`:

\mathrm{spMeasure}\ n = \mathrm{uniformOfFintype}(\mathrm{SpOmega}\ n).\mathrm{toMeasure}.

That is, a finite product of uniform (Bernoulli(1/2)) measures on a two-point space is itself the uniform (counting) measure on the product space: every one of the $2^n$ outcomes has exactly the same probability $1/2^n$ . This is the bridge that lets a measure-theoretic concentration bound proved on spMeasure n (e.g. via sub-Gaussian moment generating function machinery) be converted into a plain cardinality/counting statement about a Finset of outcomes, and vice versa.

Formalization Note. Proved via MeasureTheory.Measure.ext_of_singleton: both sides are probability measures on a finite (hence countable) type, so it suffices to check they assign the same mass to every singleton, which follows from Measure.pi_singleton and PMF.uniformOfFintype_apply after computing $2^{-n} = (\mathrm{Fintype.card}\ (\mathrm{SpOmega}\ n))^{-1}$ .

Preamble

import Definitions.Def_Komlos_RandomSignModel
import Mathlib
open Komlos MeasureTheory

Formal statement

theorem spMeasure_eq_uniform (n : ℕ) :
    spMeasure n = (PMF.uniformOfFintype (SpOmega n)).toMeasure := by sorry

Source

Elementary fact about finite product measures: an n-fold product of the uniform (Bernoulli(1/2)) measure on a 2-point set is the uniform (counting) measure on the 2^n-point product space. Standard background fact underlying probabilistic-method proofs in discrepancy theory, e.g. as used implicitly throughout N. Alon, J. Spencer, The Probabilistic Method, and in J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985) 679-706.

View graph