Triangle inequality for the GHP infimum #
Two ambient realizations are glued isometrically along the whole middle space. The pushed middle measures and images then coincide. The Lévy–Prokhorov and Hausdorff triangle inequalities bound the summed cost, and approximation of the infima gives the GHP triangle inequality.
Adapted from Freezing2/Geometry/GHPTriangle.lean in
igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit
8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).
theorem
BGW.MetricMeasure.ghpDistance_le_add_of_costs
{X Y Z : Type u}
[MetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
[CompactSpace X]
[Nonempty X]
[MetricSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[CompactSpace Y]
[Nonempty Y]
[MetricSpace Z]
[MeasurableSpace Z]
[BorelSpace Z]
[CompactSpace Z]
(μ : MeasureTheory.Measure X)
(ν : MeasureTheory.Measure Y)
(κ : MeasureTheory.Measure Z)
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
[MeasureTheory.IsProbabilityMeasure κ]
{a b : ℝ}
(ha : a ∈ ghpCosts μ ν)
(hb : b ∈ ghpCosts ν κ)
:
Two ambient costs bound the GHP distance after gluing along the whole middle space, preserving its probability measure.
theorem
BGW.MetricMeasure.ghpDistance_triangle
{X Y Z : Type u}
[MetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
[CompactSpace X]
[Nonempty X]
[MetricSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[CompactSpace Y]
[Nonempty Y]
[MetricSpace Z]
[MeasurableSpace Z]
[BorelSpace Z]
[CompactSpace Z]
(μ : MeasureTheory.Measure X)
(ν : MeasureTheory.Measure Y)
(κ : MeasureTheory.Measure Z)
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
[MeasureTheory.IsProbabilityMeasure κ]
:
The GHP infimum with summed cost obeys the triangle inequality for nonempty compact probability spaces.
theorem
BGW.MetricMeasure.ghpDistance_self
{X : Type u}
[MetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
[CompactSpace X]
(μ : MeasureTheory.Measure X)
:
A compact probability space has zero GHP distance from itself.