Measure-to-cardinality bridge for the uniform coin-flip model

Proved

spMeasure_real_coe_finset

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

combinatoricskleitmanmeasure-theoryprobabilityspencer

Let spMeasure n be the uniform i.i.d. fair-coin probability measure on SpOmega n = Fin n \to \mathrm{Bool}$, and let $S$ be any finite subset (Finset) of SpOmega n. Then the probability of $S$ under spMeasure n` is exactly its cardinality divided by the total number of outcomes:

\Pr_{\mathrm{spMeasure}\ n}[S] = \frac{|S|}{2^n}.

This is the bridge lemma converting a measure-theoretic probability statement about spMeasure n into a purely combinatorial counting statement, and vice versa: any bound proved via measure-theoretic tools (e.g. a sub-Gaussian concentration inequality bounding (spMeasure n).real {event}) becomes an explicit bound on the cardinality of the corresponding Finset of outcomes, which can then be fed into purely combinatorial results (such as extremal set theory bounds on the Hamming cube) that are not stated in measure-theoretic terms.

Formalization Note. Follows from spMeasure_eq_uniform (identifying spMeasure n with the uniform measure on the finite type SpOmega n) together with PMF.toMeasure_apply_finset (the uniform measure of a Finset equals the sum of the PMF over it) and PMF.uniformOfFintype_apply.

Preamble

import Definitions.Def_Komlos_RandomSignModel
import Theorems.Thm_spMeasure_eq_uniform
import Mathlib
open Komlos MeasureTheory

Formal statement

theorem spMeasure_real_coe_finset (n : ℕ) (S : Finset (SpOmega n)) :
    (spMeasure n).real (S : Set (SpOmega n)) = (S.card : ℝ) / (2 : ℝ) ^ n := by sorry

Source

Elementary consequence of the fact that a finite i.i.d. Bernoulli(1/2) product measure is the uniform counting measure on its (finite) sample space; the measure-to-cardinality bridge needed to connect measure-theoretic concentration inequalities (e.g. Hoeffding's inequality via HasSubgaussianMGF) to combinatorial (Finset-cardinality) statements such as Kleitman's diameter theorem, as used in the entropy-compression method of J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985) 679-706.

View graph