Quantitative comparison of pushed probability measures

Uniformly close random points have close laws in the Lévy–Prokhorov metric. A nonexpansive map contracts this metric, and weak convergence on a separable metric space implies convergence in Lévy–Prokhorov distance.

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

theorem BGW.MetricMeasure.levyProkhorovDist_map_le_of_dist_le {Ω : Type u_1} {Y : Type u_2} [MeasurableSpace Ω] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {F G : Ω → Y} (hF : Measurable F) (hG : Measurable G) {δ : ℝ} (hδ : 0 ≤ δ) (hclose : ∀ (ω : Ω), dist (F ω) (G ω) ≤ δ) : MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map F μ) (MeasureTheory.Measure.map G μ) ≤ δ

A common coupling with a deterministic distance bound gives the same Lévy–Prokhorov bound for its two marginals.

theorem BGW.MetricMeasure.levyProkhorovEDist_map_le {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {f : X → Y} (hf : LipschitzWith 1 f) : MeasureTheory.levyProkhorovEDist (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ MeasureTheory.levyProkhorovEDist μ ν

The extended Lévy–Prokhorov distance contracts under a nonexpansive map.

theorem BGW.MetricMeasure.levyProkhorovDist_map_le {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {f : X → Y} (hf : LipschitzWith 1 f) : MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ MeasureTheory.levyProkhorovDist μ ν

Lévy–Prokhorov distance between probability measures contracts under a nonexpansive map.

theorem BGW.MetricMeasure.tendsto_levyProkhorovDist_of_tendsto {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace.SeparableSpace X] {μ : ℕ → MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure X} (h : Filter.Tendsto μ Filter.atTop (nhds ν)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.levyProkhorovDist ↑(μ n) ↑ν) Filter.atTop (nhds 0)

Weak convergence of probability measures on a separable metric space gives convergence in Lévy–Prokhorov distance.