Almost everywhere continuous real encodings

Membership in countably many continuity cells encodes a separable metric space into Cantor space. The encoding is continuous away from the cell boundaries and reflects convergence. For a Polish source, its composition with the Cantor embedding is a measurable embedding into the real line. This reduces Skorokhod representation to the real quantile construction.

theorem BGW.Probability.exists_ae_continuous_real_encoding {S : Type u_1} [MetricSpace S] [PolishSpace S] [Nonempty S] [MeasurableSpace S] [BorelSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] : ∃ (g : S → ℝ), MeasurableEmbedding g ∧ (∀ᵐ (x : S) ∂μ, ContinuousAt g x) ∧ ∀ (u : ℕ → S) (x : S), Filter.Tendsto (fun (n : ℕ) => g (u n)) Filter.atTop (nhds (g x)) → Filter.Tendsto u Filter.atTop (nhds x)

A finite Borel measure on a nonempty Polish metric space admits a measurable real encoding that is continuous almost everywhere and reflects convergence of sequences.