Skorokhod representation on Polish spaces

Weakly convergent probability laws on a Polish space have measurable versions on the unit interval that converge almost surely. The proof encodes the space in the real line using small continuity cells and the Cantor set, applies real quantile coupling, then transports the resulting joint law to the unit interval.

Reference: Billingsley, Convergence of Probability Measures, second edition (1999), Theorem 6.7. The real encoding replaces the nested subinterval construction in that proof.

theorem BGW.Probability.exists_tendsto_ae_of_tendsto {S : Type u_1} [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S] {P : ℕ → MeasureTheory.ProbabilityMeasure S} {Q : MeasureTheory.ProbabilityMeasure S} (h : Filter.Tendsto P Filter.atTop (nhds Q)) : ∃ (X : ℕ → ↑unitInterval → S) (Y : ↑unitInterval → S), (∀ (n : ℕ), Measurable (X n)) ∧ Measurable Y ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (X n) MeasureTheory.volume = ↑(P n)) ∧ MeasureTheory.Measure.map Y MeasureTheory.volume = ↑Q ∧ ∀ᵐ (ω : ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (Y ω))

Skorokhod's representation theorem: weakly convergent laws on a Polish space are the laws of random variables on ([0,1], Lebesgue) converging almost surely (Billingsley 1999, Theorem 6.7; C14).