Exchangeability and Double-Sample Infrastructure

Pure mathematical infrastructure for double-sample constructions, merged samples, valid splits, and split measures. No learning-theory types.

Main definitions

• ExchangeableSample : bundles sample size m, measure μ, and probability measure proof
• DoubleSampleMeasure : D^m ⊗ D^m as product of two independent pi measures
• MergedSample : Fin (2*m) → X type alias
• mergeSamples / splitMergedSample : merge/split isomorphism
• ValidSplit : assignment of 2m indices to two groups of m
• SplitMeasure : uniform measure over valid splits
• splitFirst / splitSecond : extract groups from a merged sample

References

• Shalev-Shwartz & Ben-David, "Understanding Machine Learning", Chapter 4/6
• Kakade & Tewari, Lecture 19: Symmetrization

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

Bundle for an exchangeable sample: sample size, measure, and probability measure proof.

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

noncomputable def 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. This is the joint distribution of the training sample S and the ghost sample S'.

Construction: Measure.pi gives D^m on Fin m → X. The .prod gives the product of two such measures on (Fin m → X) × (Fin m → X).

Measurability: both factors are probability measures (by Measure.pi preserving IsProbabilityMeasure), so the product is also a probability measure.

Equations

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

@[reducible, inline]

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

Type alias for a merged sample of 2m points from X. A merged sample arises from concatenating the training sample S and ghost sample S' into a single sequence of 2m points. The key property is that under D^{2m}, all 2m points are iid, so the joint distribution is invariant under permutations.

Equations

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

noncomputable def 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. Uses Fin.append via the canonical Fin m ⊕ Fin m ≃ Fin (m + m) isomorphism, composed with the m + m = 2 * m cast.

This is the structural bridge between (Fin m → X) × (Fin m → X) and Fin (2*m) → X. The inverse is splitMergedSample.

Equations

• 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 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

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

structure ValidSplit (m : ℕ) : Type

A split of a 2m-element set into two groups of m. Represented as a function Fin (2*m) → Bool where true = first group, false = second. A valid split has exactly m elements in each group.

The set of all valid splits has cardinality Nat.choose (2*m) m.

• assign : Fin (2 * m) → Bool

  Assignment of each of 2m indices to one of two groups

• card_true : {i : Fin (2 * m) | self.assign i = true}.card = m

  Exactly m indices are assigned to the first group

def instDecidableEqValidSplit.decEq {m✝ : ℕ} (x✝ x✝¹ : ValidSplit m✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqValidSplit {m✝ : ℕ} : DecidableEq (ValidSplit m✝)

Equations

• instDecidableEqValidSplit = instDecidableEqValidSplit.decEq

@[implicit_reducible]

noncomputable instance instFintypeValidSplit (m : ℕ) : Fintype (ValidSplit m)

ValidSplit m is finite: it is a subtype of the finite type Fin (2*m) → Bool.

Equations

• instFintypeValidSplit m = Fintype.ofInjective (fun (vs : ValidSplit m) => vs.assign) ⋯

@[implicit_reducible]

instance instMeasurableSpaceValidSplit (m : ℕ) : MeasurableSpace (ValidSplit m)

Discrete measurable space on ValidSplit (all sets measurable).

Equations

• instMeasurableSpaceValidSplit m = ⊤

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

The uniform measure over all valid splits of 2m elements into two groups of m. This is the key construction for the exchangeability argument (Approach A).

Under D^{2m}, conditioning on the merged sample z and averaging over all valid splits gives the same distribution as D^m ⊗ D^m. This is because D^{2m} is invariant under permutations of coordinates.

The measure assigns weight 1/C(2m,m) to each valid split.

MEASURABILITY NOTE: ValidSplit m is a finite type (subtype of Fin (2*m) → Bool), so all sets are measurable under the discrete σ-algebra.

Equations

• SplitMeasure m = if _h : Fintype.card (ValidSplit m) = 0 then 0 else (↑(Fintype.card (ValidSplit m)))⁻¹ • ∑ vs : ValidSplit m, MeasureTheory.Measure.dirac vs

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

Given a merged sample z and a valid split, extract the first group (training sample).

Equations

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

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

Given a merged sample z and a valid split, extract the second group (ghost sample).

Equations

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