The Gromov–Hausdorff–Prokhorov infimum

The cost is the sum of Lévy–Prokhorov and Hausdorff distances after isometric embeddings into one ambient metric space. Hausdorff distance uses the images of the whole carriers, with no full-support assumption on the measures. The spaces and ambient realizations lie in the same universe.

The intended GHP setting is nonempty compact metric spaces with Borel probability measures. The raw infimum below also accepts arbitrary measures, as in the source. This module supplies nonnegativity and upper bounds on represented spaces; the triangle inequality, separation and passage to isometry classes are separate obligations.

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

def BGW.MetricMeasure.ghpCosts {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : Set ℝ

The costs of all common ambient realizations in the same universe, with their Borel measurable structures and isometric embeddings of the whole carriers.

The compactness and Borel assumptions are not used by the formula; they fix its domain. Compactness of both carriers, together with their nonemptiness (automatic for the carriers of probability measures, as in CompactMeasuredSpace), makes the Hausdorff distance between the embedded carriers finite. Compactness alone does not exclude an empty carrier facing a nonempty one, in which case Mathlib's real hausdorffDist takes its default value 0. The Borel assumptions make the isometric embeddings measurable, so that the pushforward measures in the Lévy–Prokhorov term are meaningful (Measure.map of a non-measurable map is 0); they play no role in the finiteness of the Hausdorff term.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.MetricMeasure.ghpDistance {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : ℝ

The GHP infimum on represented compact measured spaces, before passage to measure-preserving isometry classes. Its compactness and Borel assumptions fix the domain, as explained for ghpCosts: they are what makes the costs meaningful, for nonempty carriers.

Equations

• BGW.MetricMeasure.ghpDistance μ ν = sInf (BGW.MetricMeasure.ghpCosts μ ν)

theorem BGW.MetricMeasure.ghpCosts_bddBelow {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : BddBelow (ghpCosts μ ν)

theorem BGW.MetricMeasure.ghpCosts_nonempty {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : (ghpCosts μ ν).Nonempty

theorem BGW.MetricMeasure.ghpDistance_nonneg {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : 0 ≤ ghpDistance μ ν

theorem BGW.MetricMeasure.ghpDistance_le_of_isometries {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (Z : Type u) [MetricSpace Z] (i : X → Z) (j : Y → Z) (hi : Isometry i) (hj : Isometry j) : ghpDistance μ ν ≤ MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map i μ) (MeasureTheory.Measure.map j ν) + Metric.hausdorffDist (Set.range i) (Set.range j)

Any common ambient realization gives an upper bound for the GHP infimum.

theorem BGW.MetricMeasure.ghpDistance_le_of_approx {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [CompactSpace X] [BorelSpace X] [CompactSpace Y] [BorelSpace Y] [Nonempty X] [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) : ghpDistance μ ν ≤ 2 * δ + r + p

A measurable map with small distortion, dense image and close pushed measure gives a quantitative GHP upper bound.