Prokhorov distance under compact isometric embeddings

A compact isometric image is Borel, so every source Borel test set can be transported to the ambient space. Its thickening has exactly the original preimage. Together with contraction this gives equality of Prokhorov distances.

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

theorem BGW.MetricMeasure.preimage_thickening_image_of_isometry {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Isometry f) (r : ℝ) (B : Set X) : f ⁻¹' Metric.thickening r (f '' B) = Metric.thickening r B

theorem BGW.MetricMeasure.levyProkhorovEDist_map_isometry {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {f : X → Y} (hf : Isometry f) : MeasureTheory.levyProkhorovEDist (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) = MeasureTheory.levyProkhorovEDist μ ν

A compact isometric embedding preserves the full extended Prokhorov distance, not merely its vanishing or topology.

theorem BGW.MetricMeasure.levyProkhorovDist_map_isometry {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {f : X → Y} (hf : Isometry f) : MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) = MeasureTheory.levyProkhorovDist μ ν

The real Prokhorov distance is likewise unchanged.