Double-sample measure and merge/split isomorphism

Core constructions for the symmetrization / exchangeability pipeline: an ExchangeableSample bundle, the DoubleSampleMeasure product, the MergedSample abbrev on Fin (2*m) → X, and the mergeSamples / splitMergedSample isomorphism between (Fin m → X) × (Fin m → X) and Fin (2*m) → X.

structure ProbabilityTheory.ExchangeableSample {X : Type u_1} [MeasurableSpace X] : Type u_1

Bundle: sample size, measure, and probability-measure proof.

• m : ℕ
• μ : MeasureTheory.Measure X
• hμ : MeasureTheory.IsProbabilityMeasure self.μ

noncomputable def ProbabilityTheory.DoubleSampleMeasure {X : Type u} [MeasurableSpace X] (D : MeasureTheory.Measure X) (m : ℕ) : MeasureTheory.Measure ((Fin m → X) × (Fin m → X))

The double sample measure D^m ⊗ D^m: the product of two independent m-fold product measures. Joint distribution of training + ghost samples.

Equations

• ProbabilityTheory.DoubleSampleMeasure D m = (MeasureTheory.Measure.pi fun (x : Fin m) => D).prod (MeasureTheory.Measure.pi fun (x : Fin m) => D)

@[reducible, inline]

abbrev ProbabilityTheory.MergedSample (X : Type u) (m : ℕ) : Type u

Type alias for a merged sample of 2m points from X.

Equations

• ProbabilityTheory.MergedSample X m = (Fin (2 * m) → X)

noncomputable def ProbabilityTheory.mergeSamples {X : Type u} {m : ℕ} (p : (Fin m → X) × (Fin m → X)) : MergedSample X m

Merge two samples of size m into a single sample of size 2m.

Equations

• ProbabilityTheory.mergeSamples p i = if h : ↑(Fin.cast ⋯ i) < m then p.1 ⟨↑(Fin.cast ⋯ i), h⟩ else p.2 ⟨↑(Fin.cast ⋯ i) - m, ⋯⟩

noncomputable def ProbabilityTheory.splitMergedSample {X : Type u} {m : ℕ} (z : MergedSample X m) : (Fin m → X) × (Fin m → X)

Split a merged sample of 2m points back into two samples of size m. Inverse of mergeSamples.

Equations

• ProbabilityTheory.splitMergedSample z = (fun (i : Fin m) => z (Fin.cast ⋯ (Fin.castAdd m i)), fun (i : Fin m) => z (Fin.cast ⋯ (Fin.natAdd m i)))