Lean: ProbabilityTheory.ExchangeableSample

A bundle \(\langle m, \mu , \mathrm{IsProbabilityMeasure}\, \mu \rangle \) where \(m \in \mathbb {N}\) is the sample size and \(\mu \) is a probability measure on the sample space. Used with the product measure \(\mu ^{\otimes 2m}\) as the natural exchangeable double-sample domain [ 13 , § 11 ] , [ 5 , Ch. 12 ] .

Lean: ProbabilityTheory.ValidSplit

\(s : \mathrm{Fin}(2m) \to \mathrm{Bool}\) is a valid split iff exactly \(m\) of its values are true. There are \(\binom {2m}{m}\) valid splits (Vapnik-Chervonenkis double-sample [ 23 ] ).

Lean: ProbabilityTheory.SplitMeasure

The uniform probability measure on the set of valid splits. This is the symmetrization measure for the double-sample trick [ 23 ] , [ 5 , Ch. 12 ] .