Transport of the rooted GHP infimum

Precomposing an ambient realization by a surjective isometry preserves its whole image, pushed measure and distinguished point. Thus the entire set of rooted costs is invariant under transport of both the measure and the root.

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

theorem BGW.MetricMeasure.rootedGHPCosts_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') (x : X) (y : Y) : rootedGHPCosts (MeasureTheory.Measure.map (⇑e) μ) ν (e x) y ⊆ rootedGHPCosts μ ν x y

theorem BGW.MetricMeasure.rootedGHPCosts_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') (x : X) (y : Y) : rootedGHPCosts (MeasureTheory.Measure.map (⇑e) μ) ν (e x) y = rootedGHPCosts μ ν x y

Transport preserves the complete set of rooted ambient costs.

theorem BGW.MetricMeasure.rootedGHPDistance_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') (x : X) (y : Y) : rootedGHPDistance (MeasureTheory.Measure.map (⇑e) μ) ν (e x) y = rootedGHPDistance μ ν x y

theorem BGW.MetricMeasure.rootedGHPDistance_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') (y : Y) (x : X) : rootedGHPDistance ν (MeasureTheory.Measure.map (⇑e) μ) y (e x) = rootedGHPDistance ν μ y x

theorem BGW.MetricMeasure.rootedGHPDistance_eq_zero_of_measured_isometry {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) (x : X) (y : Y) (e : X ≃ᵢ Y) (hμ : MeasureTheory.Measure.map (⇑e) μ = ν) (hroot : e x = y) : rootedGHPDistance μ ν x y = 0

A measured isometry preserving the root gives zero rooted distance.