Transport of almost sure representations to the unit interval

An almost surely convergent sequence of Polish-valued random variables on any probability space can be realized on the unit interval, with the same joint law. Thus the choice of the unit interval as the source of a Skorokhod representation is independent of the construction of its coupling.

theorem BGW.Probability.exists_tendsto_ae_unitInterval_of_commonSpace {S : Type u_1} {Ω : Type u_2} [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S] [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → S} {Y : Ω → S} (hX : ∀ (n : ℕ), Measurable (X n)) (hY : Measurable Y) (hconv : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (Y ω))) : ∃ (X' : ℕ → ↑unitInterval → S) (Y' : ↑unitInterval → S), (∀ (n : ℕ), Measurable (X' n)) ∧ Measurable Y' ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (X' n) MeasureTheory.volume = MeasureTheory.Measure.map (X n) μ) ∧ MeasureTheory.Measure.map Y' MeasureTheory.volume = MeasureTheory.Measure.map Y μ ∧ ∀ᵐ (ω : ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => X' n ω) Filter.atTop (nhds (Y' ω))

Transfer an almost surely convergent common-space representation to Lebesgue measure on the unit interval. No standard Borel assumption on the original probability space is needed.