SplitMeasure: uniform measure on valid splits, with first/second projections

Conditioning a D^{2m} sample on the merged sample z and averaging over all ValidSplit m outcomes recovers D^m ⊗ D^m, because D^{2m} is invariant under coordinate permutations. SplitMeasure m assigns weight 1 / C(2m, m) to each valid split.

noncomputable def ProbabilityTheory.SplitMeasure (m : ℕ) : MeasureTheory.Measure (ValidSplit m)

Uniform measure over all valid splits of 2m into two groups of m.

The core construction for the exchangeability argument: with weight 1 / Fintype.card (ValidSplit m) on each split, the Dirac sum gives a probability measure on the finite, discrete space ValidSplit m.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.splitFirst {X : Type u} {m : ℕ} (z : MergedSample X m) (_vs : ValidSplit m) : Fin m → X

First-group projection of a merged sample under a valid split.

Equations

• ProbabilityTheory.splitFirst z _vs i = z (Fin.cast ⋯ (Fin.castAdd m i))

def ProbabilityTheory.splitSecond {X : Type u} {m : ℕ} (z : MergedSample X m) (_vs : ValidSplit m) : Fin m → X

Second-group projection of a merged sample under a valid split.

Equations

• ProbabilityTheory.splitSecond z _vs i = z (Fin.cast ⋯ (Fin.natAdd m i))