Conditional couplings for the separable representation theorem

A countable measurable partition of S gives, for two probability measures μ and ν, a conditional coupling driven by a shared uniform variable u. Given the current point y, in the cell A i, the coupled point stays in the cell (drawn from μ conditioned on A i) when u is below the stay probability of that cell, and is otherwise drawn from the residual law. The probability of landing in different cells is bounded by the cell-mass defect cellDefect. Iterating these kernels over a sequence of partitions gives a trajectory construction over the base S × unitInterval, with the uniform variable shared across all times.

See Dudley, "Distances of probability measures and random variables" (1968), and Real Analysis and Probability (2002), Theorem 11.7.2.

noncomputable def BGW.Probability.partitionIndex {S : Type u_1} (A : ℕ → Set S) (hA : ⋃ (i : ℕ), A i = Set.univ) (x : S) : ℕ

The index of the unique cell of a countable measurable partition containing a point.

Equations

• BGW.Probability.partitionIndex A hA x = Nat.find ⋯

theorem BGW.Probability.partitionIndex_mem {S : Type u_1} {A : ℕ → Set S} {hA : ⋃ (i : ℕ), A i = Set.univ} (x : S) : x ∈ A (partitionIndex A hA x)

A point lies in the cell indexed by its partitionIndex.

noncomputable def BGW.Probability.cellDefect {S : Type u_1} [MeasurableSpace S] (μ ν : MeasureTheory.Measure S) (A : ℕ → Set S) : ENNReal

The one-sided cell-mass defect cellDefect used to control different-cell probability.

Equations

• BGW.Probability.cellDefect μ ν A = ∑' (i : ℕ), (ν (A i) - min (μ (A i)) (ν (A i)))

noncomputable def BGW.Probability.cellStayProbability {S : Type u_1} [MeasurableSpace S] (μ ν : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure ν] (A : ℕ → Set S) (i : ℕ) : ↑unitInterval

The probability of using the conditional law on a cell, represented in the unit interval.

Equations

• BGW.Probability.cellStayProbability μ ν A i = ⟨(min (μ (A i)) (ν (A i)) * (ν (A i))⁻¹).toReal, ⋯⟩

theorem BGW.Probability.exists_uniform_coupling_of_partitions {S : Type u_1} [MeasurableSpace S] (μ : ℕ → MeasureTheory.Measure S) (ν : MeasureTheory.Measure S) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] [MeasureTheory.IsProbabilityMeasure ν] (A : ℕ → ℕ → Set S) (hmeas : ∀ (n i : ℕ), MeasurableSet (A n i)) (hdisj : ∀ (n : ℕ), Pairwise (Function.onFun Disjoint (A n))) (hcover : ∀ (n : ℕ), ⋃ (i : ℕ), A n i = Set.univ) : ∃ (ρ : MeasureTheory.Measure ((S × ↑unitInterval) × (ℕ → S))), MeasureTheory.IsProbabilityMeasure ρ ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (fun (z : (S × ↑unitInterval) × (ℕ → S)) => z.2 n) ρ = μ n) ∧ MeasureTheory.Measure.map Prod.fst ρ = ν.prod MeasureTheory.volume ∧ ∀ (n i : ℕ), ρ {z : (S × ↑unitInterval) × (ℕ → S) | z.1.1 ∈ A n i ∧ z.1.2 < cellStayProbability (μ n) ν (A n) i ∧ partitionIndex (A n) ⋯ z.1.1 ≠ partitionIndex (A n) ⋯ (z.2 n)} = 0

Couplings driven by one uniform variable on every cell. In addition to exact marginals, the common-branch mismatch events are null, which lets a later diagonal argument share the uniform variable across all times.