Separation for the exact measured GHP distance

Near-zero actual ambient costs give approximate maps between the entire compact carriers. A compact uniform limit is a surjective isometry. Uniform closeness in the original ambient realizations, together with their vanishing Prokhorov costs, proves that this isometry preserves the probability measures. Thus no points outside the measure supports are discarded.

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

structure BGW.MetricMeasure.GHPCoupling (X Y : Type u) [MetricSpace X] [MetricSpace Y] : Type (u + 1)

An actual common ambient metric realization of two spaces.

• ambient : Type u

  The common ambient carrier realizing both spaces.

• metric : MetricSpace self.ambient

  The metric on the common ambient carrier.

• left : X → self.ambient

  The isometric embedding of the whole left-hand space.

• right : Y → self.ambient

  The isometric embedding of the whole right-hand space.

• left_isometry : Isometry self.left
• right_isometry : Isometry self.right

@[instance_reducible]

instance BGW.MetricMeasure.GHPCoupling.instMetricSpaceAmbient {X Y : Type u} [MetricSpace X] [MetricSpace Y] (C : GHPCoupling X Y) : MetricSpace C.ambient

Equations

• C.instMetricSpaceAmbient = C.metric

@[instance_reducible]

noncomputable instance BGW.MetricMeasure.GHPCoupling.instMeasurableSpaceAmbient {X Y : Type u} [MetricSpace X] [MetricSpace Y] (C : GHPCoupling X Y) : MeasurableSpace C.ambient

Equations

• C.instMeasurableSpaceAmbient = borel C.ambient

instance BGW.MetricMeasure.GHPCoupling.instBorelSpaceAmbient {X Y : Type u} [MetricSpace X] [MetricSpace Y] (C : GHPCoupling X Y) : BorelSpace C.ambient

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

The sum of the Lévy–Prokhorov cost of the pushed measures and the Hausdorff cost of the embedded whole spaces.

Equations

• C.cost μ ν = MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map C.left μ) (MeasureTheory.Measure.map C.right ν) + Metric.hausdorffDist (Set.range C.left) (Set.range C.right)

theorem BGW.MetricMeasure.GHPCoupling.exists_approximation {X Y : Type u} [MetricSpace X] [MetricSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [CompactSpace X] [CompactSpace Y] [Nonempty X] [Nonempty Y] (C : GHPCoupling X Y) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) {ε : ℝ} (hC : C.cost μ ν < ε) : ∃ (f : X → Y), (∀ (x : X), dist (C.left x) (C.right (f x)) < ε) ∧ (∀ (x y : X), |dist (f x) (f y) - dist x y| ≤ 2 * ε) ∧ ∀ (y : Y), ∃ (x : X), dist y (f x) ≤ 2 * ε

A small actual ambient cost supplies approximate isometries on all points. The chosen maps themselves need no measurability assumption.

theorem BGW.MetricMeasure.exists_ghpCoupling_cost_lt_of_eq_zero {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) (hz : ghpDistance μ ν = 0) {ε : ℝ} (hε : 0 < ε) : ∃ (C : GHPCoupling X Y), C.cost μ ν < ε

The GHP infimum supplies actual ambient realizations with arbitrarily small summed costs when the distance is zero.

theorem BGW.MetricMeasure.exists_measured_isometry_of_ghpDistance_eq_zero {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [Nonempty Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hz : ghpDistance μ ν = 0) : ∃ (e : X ≃ᵢ Y), MeasureTheory.Measure.map (⇑e) μ = ν

Zero GHP distance forces a measure-preserving isometry of the entire compact spaces. Compactness controls geometry and the ambient Prokhorov bounds determine the measure of the resulting isometry.

theorem BGW.MetricMeasure.ghpDistance_eq_zero_iff_measured_isometry {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [Nonempty X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [Nonempty Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : ghpDistance μ ν = 0 ↔ ∃ (e : X ≃ᵢ Y), MeasureTheory.Measure.map (⇑e) μ = ν

Separation is with respect to whole-space measured isometry, exactly as for whole-space measured isometry.