53 Communication Complexity — Coin Tape
53.1 Overview
This module introduces the type of finite coin sequences used in randomised communication complexity and equips it with the uniform probability measure. A coin tape of length \(n\) is a sequence of \(n\) independent fair coin flips; the module provides the canonical MeasureSpace instance whose volume is the uniform measure on all such sequences, together with a proof that this measure is a probability measure.
53.2 Declarations
\(\texttt{CoinTape}(n)\) is the type \(\mathrm{Fin}\, n \to \mathrm{Bool}\), i.e. the set of all binary strings of length \(n\), representing the \(2^n\) possible outcomes of \(n\) independent fair coin flips.