Reduction from pseudometric spaces to their separation quotients

The canonical section from the separation quotient to a pseudometric space is Borel measurable. Consequently, a separable-metric representation theorem can be transported back to the original pseudometric space without changing either the laws or almost-sure convergence. See Dudley, "Distances of probability measures and random variables" (1968), and Real Analysis and Probability (2002), Theorem 11.7.2.

theorem BGW.Probability.exists_probabilitySpace_tendsto_ae_of_tendsto_of_metric {S : Type u} [PseudoMetricSpace S] [TopologicalSpace.SeparableSpace S] [MeasurableSpace S] [BorelSpace S] (hMetric : ∀ {T : Type u} [inst : MetricSpace T] [TopologicalSpace.SeparableSpace T] [inst_2 : MeasurableSpace T] [inst_3 : BorelSpace T] {P : ℕ → MeasureTheory.ProbabilityMeasure T} {Q : MeasureTheory.ProbabilityMeasure T}, Filter.Tendsto P Filter.atTop (nhds Q) → ∃ (Ω : Type u) (x : MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω) (_ : MeasureTheory.IsProbabilityMeasure μ) (X : ℕ → Ω → T) (Y : Ω → T), (∀ (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 ω))) {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 ω))

Conditional reduction of the separable representation theorem to the metric case. Any suitable metric representation can be lifted through the canonical quotient section.