Completeness of the whole-space GHP metric

Fast successive couplings are realized in one complete ambient space. Their compact images have a Hausdorff limit and all lie in a compact hull. Pushed probability measures have a weakly convergent subsequence on that hull; its ambient pushforward is carried by the limiting compact set. Restriction produces a probability on that entire set. This gives a GHP limit and hence completeness, without requiring full support or separability of the initially constructed ambient space.

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

theorem BGW.MetricMeasure.exists_measured_limit_of_geometric_couplings (X : ℕ → CompactMeasuredSpace) (C : (n : ℕ) → GHPCoupling (X n).carrier (X (n + 1)).carrier) (hC : ∀ (n : ℕ), (C n).cost ↑(X n).law ↑(X (n + 1)).law < (1 / 2) ^ n) : ∃ (Y : CompactMeasuredSpace), Filter.Tendsto (fun (n : ℕ) => toMeasuredGHSpace (X n)) Filter.atTop (nhds (toMeasuredGHSpace Y))

A geometric sequence of actual measured coupling costs has a limit represented by a compact metric space with a Borel probability measure.

instance BGW.MetricMeasure.MeasuredGHSpace.instCompleteSpace : CompleteSpace MeasuredGHSpace

The exact whole-space GHP metric is complete.

theorem BGW.MetricMeasure.MeasuredGHSpace.polishSpace : PolishSpace MeasuredGHSpace

The source whole-space quotient, with its already defined GHP topology, is a Polish space.