The rooted Gromov–Hausdorff–Prokhorov infimum

A rooted ambient cost is the distance between the embedded roots plus the existing Lévy–Prokhorov and whole-carrier Hausdorff cost. In particular, the root contribution is an actual distance, not the Prokhorov distance between Dirac measures. Roots need not belong to the support of the measure.

All carriers and ambient realizations lie in the same universe. As for the unrooted infimum, the raw definitions accept arbitrary measures; the intended metric setting consists of compact nonempty Borel probability spaces.

This extends the existing GHPCoupling and unrooted infimum, adapted from Freezing2/Geometry/GHPSeparation.lean and GromovHausdorffProkhorov.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

noncomputable def BGW.MetricMeasure.GHPCoupling.rootedCost {X Y : Type u} [MetricSpace X] [MetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] (C : GHPCoupling X Y) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (x : X) (y : Y) : ℝ

Root distance plus the existing summed measured GHP cost.

Equations

• C.rootedCost μ ν x y = dist (C.left x) (C.right y) + C.cost μ ν

theorem BGW.MetricMeasure.GHPCoupling.rootedCost_nonneg {X Y : Type u} [MetricSpace X] [MetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] (C : GHPCoupling X Y) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (x : X) (y : Y) : 0 ≤ C.rootedCost μ ν x y

def BGW.MetricMeasure.rootedGHPCosts {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) (x : X) (y : Y) : Set ℝ

Costs of common ambient isometric realizations, including the distance between roots.

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 RootedCompactMeasuredSpace), 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

• BGW.MetricMeasure.rootedGHPCosts μ ν x y = {r : ℝ | ∃ (C : BGW.MetricMeasure.GHPCoupling X Y), r = C.rootedCost μ ν x y}

noncomputable def BGW.MetricMeasure.rootedGHPDistance {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) (x : X) (y : Y) : ℝ

The rooted GHP infimum on represented compact measured spaces. Its compactness and Borel assumptions fix the domain, as explained for rootedGHPCosts.

Equations

• BGW.MetricMeasure.rootedGHPDistance μ ν x y = sInf (BGW.MetricMeasure.rootedGHPCosts μ ν x y)

theorem BGW.MetricMeasure.rootedGHPCosts_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) (x : X) (y : Y) : BddBelow (rootedGHPCosts μ ν x y)

theorem BGW.MetricMeasure.rootedGHPCosts_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) (x : X) (y : Y) : (rootedGHPCosts μ ν x y).Nonempty

theorem BGW.MetricMeasure.rootedGHPDistance_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) (x : X) (y : Y) : 0 ≤ rootedGHPDistance μ ν x y

theorem BGW.MetricMeasure.rootedGHPDistance_le_of_coupling {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) (x : X) (y : Y) (C : GHPCoupling X Y) : rootedGHPDistance μ ν x y ≤ C.rootedCost μ ν x y

Every actual ambient realization gives an upper bound for the rooted infimum.

theorem BGW.MetricMeasure.rootedGHPDistance_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) (x : X) (y : Y) (Z : Type u) [MetricSpace Z] (i : X → Z) (j : Y → Z) (hi : Isometry i) (hj : Isometry j) : rootedGHPDistance μ ν x y ≤ dist (i x) (j y) + (MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map i μ) (MeasureTheory.Measure.map j ν) + Metric.hausdorffDist (Set.range i) (Set.range j))

A common ambient pair of isometries bounds the rooted GHP distance.

theorem BGW.MetricMeasure.rootedGHPCosts_comm {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) (x : X) (y : Y) : rootedGHPCosts μ ν x y = rootedGHPCosts ν μ y x

theorem BGW.MetricMeasure.rootedGHPDistance_comm {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) (x : X) (y : Y) : rootedGHPDistance μ ν x y = rootedGHPDistance ν μ y x

theorem BGW.MetricMeasure.ghpDistance_le_rootedGHPDistance {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) (x : X) (y : Y) : ghpDistance μ ν ≤ rootedGHPDistance μ ν x y

Forgetting the roots can only decrease the represented distance.