Documentation

BGW.MetricMeasure.RootedGHPTriangle

Triangle inequality for the rooted GHP infimum #

The existing gluing of two ambient realizations identifies the whole middle carrier. In particular, both images of its root agree. The ordinary distance triangle inequality controls the root contribution, alongside the existing Hausdorff and Lévy–Prokhorov estimates.

The proof extends BGW.MetricMeasure.GHPTriangle, adapted from Freezing2/Geometry/GHPTriangle.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0). No quotient metric or separation theorem is asserted in this module.

source
theorem BGW.MetricMeasure.rootedGHPDistance_le_add_of_costs {X Y Z : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [MetricSpace Z] [MeasurableSpace Z] [BorelSpace Z] [CompactSpace Z] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (κ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure κ] (x : X) (y : Y) (z : Z) {a b : ℝ} (ha : a ∈ rootedGHPCosts μ ν x y) (hb : b ∈ rootedGHPCosts ν κ y z) :
rootedGHPDistance μ κ x z ≤ a + b

Glue two rooted ambient costs along the whole middle compact space.

source
theorem BGW.MetricMeasure.rootedGHPDistance_triangle {X Y Z : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [MetricSpace Z] [MeasurableSpace Z] [BorelSpace Z] [CompactSpace Z] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (κ : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure κ] (x : X) (y : Y) (z : Z) :
rootedGHPDistance μ κ x z ≤ rootedGHPDistance μ ν x y + rootedGHPDistance ν κ y z

The rooted summed-cost infimum satisfies the triangle inequality.

source
theorem BGW.MetricMeasure.rootedGHPDistance_self {X : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] (μ : MeasureTheory.Measure X) (x : X) :
rootedGHPDistance μ μ x x = 0

A rooted compact probability space has zero distance from itself.