Transport of the GHP infimum by measured isometries

Precomposition by a surjective isometry preserves each ambient cost, including the pushed measure and the entire embedded image. Hence the infimum is invariant under measure-preserving isometry equivalences and symmetric in its arguments.

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

theorem BGW.MetricMeasure.ghpCosts_map_isometryEquiv_subset {X X' Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace X'] [MeasurableSpace X'] [BorelSpace X'] [CompactSpace X'] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (e : X ≃ᵢ X') : ghpCosts (MeasureTheory.Measure.map (⇑e) μ) ν ⊆ ghpCosts μ ν

theorem BGW.MetricMeasure.ghpCosts_map_isometryEquiv {X X' Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace X'] [MeasurableSpace X'] [BorelSpace X'] [CompactSpace X'] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (e : X ≃ᵢ X') : ghpCosts (MeasureTheory.Measure.map (⇑e) μ) ν = ghpCosts μ ν

Isometry transport preserves the complete set of ambient costs. The Borel structure in each witness is induced by that witness's metric.

theorem BGW.MetricMeasure.ghpDistance_map_isometryEquiv {X X' Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace X'] [MeasurableSpace X'] [BorelSpace X'] [CompactSpace X'] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (e : X ≃ᵢ X') : ghpDistance (MeasureTheory.Measure.map (⇑e) μ) ν = ghpDistance μ ν

theorem BGW.MetricMeasure.ghpDistance_eq_of_isometryEquiv {X X' Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace X'] [MeasurableSpace X'] [BorelSpace X'] [CompactSpace X'] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (μ : MeasureTheory.Measure X) (μ' : MeasureTheory.Measure X') (ν : MeasureTheory.Measure Y) (e : X ≃ᵢ X') (hμ : MeasureTheory.Measure.map (⇑e) μ = μ') : ghpDistance μ ν = ghpDistance μ' ν

A measure-preserving isometry equivalence preserves the represented GHP distance.

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

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

theorem BGW.MetricMeasure.ghpDistance_map_isometryEquiv_right {X X' Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MetricSpace X'] [MeasurableSpace X'] [BorelSpace X'] [CompactSpace X'] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (ν : MeasureTheory.Measure Y) (μ : MeasureTheory.Measure X) (e : X ≃ᵢ X') : ghpDistance ν (MeasureTheory.Measure.map (⇑e) μ) = ghpDistance ν μ

Isometry transport in the right argument also preserves the distance.