Dudley's representation theorem on separable spaces

A single uniform variable is shared by all the conditional couplings. At partition level k, a different-cell event outside one universal null set implies either that this variable exceeds 1 - 2 ^ (-k) or that the limiting random variable lies outside a fixed finite family of cells. These events are summable in k. Borel--Cantelli therefore gives small common-cell distance at all sufficiently large times, hence almost-sure convergence.

References

• R. M. Dudley, "Distances of probability measures and random variables", Ann. Math. Statist. 39 (1968), 1563--1572.
• R. M. Dudley, Real Analysis and Probability, Cambridge University Press, 2002, Theorem 11.7.2.

theorem BGW.Probability.exists_probabilitySpace_tendsto_ae_of_tendsto_metric {S : Type u} [MetricSpace S] [TopologicalSpace.SeparableSpace S] [MeasurableSpace S] [BorelSpace S] {P : ℕ → MeasureTheory.ProbabilityMeasure S} {Q : MeasureTheory.ProbabilityMeasure S} (h : Filter.Tendsto P Filter.atTop (nhds Q)) : ∃ (Ω : Type u) (x : MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) (_ : MeasureTheory.IsProbabilityMeasure μ) (X : ℕ → Ω → S) (Y : Ω → S), (∀ (n : ℕ), Measurable (X n)) ∧ Measurable Y ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (X n) μ = ↑(P n)) ∧ MeasureTheory.Measure.map Y μ = ↑Q ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (Y ω))

Dudley's representation theorem in the metric case, with the augmented sample space (S × unitInterval) × (ℕ → S).

theorem BGW.Probability.exists_probabilitySpace_tendsto_ae_of_tendsto {S : Type u} [PseudoMetricSpace S] [TopologicalSpace.SeparableSpace S] [MeasurableSpace S] [BorelSpace S] {P : ℕ → MeasureTheory.ProbabilityMeasure S} {Q : MeasureTheory.ProbabilityMeasure S} (h : Filter.Tendsto P Filter.atTop (nhds Q)) : ∃ (Ω : Type u) (x : MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) (_ : MeasureTheory.IsProbabilityMeasure μ) (X : ℕ → Ω → S) (Y : Ω → S), (∀ (n : ℕ), Measurable (X n)) ∧ Measurable Y ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (X n) μ = ↑(P n)) ∧ MeasureTheory.Measure.map Y μ = ↑Q ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (Y ω))

Dudley (1968): weak convergence of laws on a separable pseudometric space S with its Borel σ-algebra implies a.s. convergent random variables on some probability space (Billingsley 1999, Theorem 6.7 is the Polish/[0,1] case).