A common metric realization of measured approximations

A map of small distortion produces isometric embeddings into a common metric space. These embeddings control both Hausdorff distance between the whole images and Lévy–Prokhorov distance between the pushed probability measures.

Adapted from Freezing2/Geometry/MeasuredGluing.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

theorem BGW.MetricMeasure.exists_measured_gluing {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [Nonempty Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (f : X → Y) (hf : Measurable f) {δ r p : ℝ} (hδ : 0 < δ) (hdis : ∀ (x x' : X), |dist x x' - dist (f x) (f x')| ≤ 2 * δ) (hdense : ∀ (y : Y), ∃ (x : X), dist y (f x) ≤ r) (hprob : MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map f μ) ν ≤ p) : ∃ (m : MetricSpace (X ⊕ Y)), Isometry Sum.inl ∧ Isometry Sum.inr ∧ Metric.hausdorffDist (Set.range Sum.inl) (Set.range Sum.inr) ≤ δ + r ∧ MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map Sum.inl μ) (MeasureTheory.Measure.map Sum.inr ν) ≤ δ + p

Small distortion, a dense image and close pushed measures give a common metric space with simultaneous Hausdorff and Lévy–Prokhorov bounds.