Measured cost control in a common ambient space #
The isometric factorizations of successive couplings preserve their Hausdorff contributions and do not increase their Prokhorov contributions. The single complete ambient space therefore retains both parts of every supplied cost.
Adapted from Freezing2/Geometry/GHPChainMeasures.lean in
igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit
8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).
theorem
BGW.MetricMeasure.GHPCoupling.cost_le_after_isometry
{X Y Z : Type u}
[MetricSpace X]
[MeasurableSpace X]
[BorelSpace X]
[MetricSpace Y]
[MeasurableSpace Y]
[BorelSpace Y]
[MetricSpace Z]
[MeasurableSpace Z]
[BorelSpace Z]
(C : GHPCoupling X Y)
(μ : MeasureTheory.Measure X)
(ν : MeasureTheory.Measure Y)
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
(j : C.ambient → Z)
(hj : Isometry j)
:
MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map (j ∘ C.left) μ) (MeasureTheory.Measure.map (j ∘ C.right) ν) + Metric.hausdorffDist (Set.range (j ∘ C.left)) (Set.range (j ∘ C.right)) ≤ C.cost μ ν
An isometric embedding of a coupling's ambient space cannot increase its measured cost. The pushed measures are exactly the original marginals followed by the same ambient embedding.
theorem
BGW.MetricMeasure.GHPChain.exists_complete_measured_realization
(X : ℕ → Type u)
[(n : ℕ) → MetricSpace (X n)]
[∀ (n : ℕ), Nonempty (X n)]
[(n : ℕ) → MeasurableSpace (X n)]
[∀ (n : ℕ), BorelSpace (X n)]
(μ : (n : ℕ) → MeasureTheory.Measure (X n))
[∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)]
(C : (n : ℕ) → GHPCoupling (X n) (X (n + 1)))
:
∃ (Z : Type u) (m : MetricSpace Z) (_ : CompleteSpace Z) (ι : (n : ℕ) → X n → Z),
(∀ (n : ℕ), Isometry (ι n)) ∧ ∀ (n : ℕ),
MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map (ι n) (μ n))
(MeasureTheory.Measure.map (ι (n + 1)) (μ (n + 1))) + Metric.hausdorffDist (Set.range (ι n)) (Set.range (ι (n + 1))) ≤ (C n).cost (μ n) (μ (n + 1))
All adjacent measured costs are simultaneously controlled in one genuine complete metric space with its metric-induced Borel structure.