Completeness of the existing rooted GHP metric

The successive rooted couplings are glued in one complete ambient space. The same isometric factorizations retain their root distances and their Lévy–Prokhorov and whole-carrier Hausdorff costs. The roots form a Cauchy sequence, whose limit lies in the limiting compact carrier. The limiting probability is constructed on that entire carrier, without requiring the root to belong to its support.

This extends BGW.MetricMeasure.GHPCompleteness and its common-space proof, adapted from Freezing2/Geometry/GHPCompleteness.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0). No new quotient, metric, topology, or measurable-space instance is introduced.

theorem BGW.MetricMeasure.exists_rooted_measured_limit_of_geometric_couplings (X : ℕ → RootedCompactMeasuredSpace) (C : (n : ℕ) → GHPCoupling (X n).space.carrier (X (n + 1)).space.carrier) (hC : ∀ (n : ℕ), (C n).rootedCost (↑(X n).space.law) (↑(X (n + 1)).space.law) (X n).root (X (n + 1)).root < (1 / 2) ^ n) : ∃ (Y : RootedCompactMeasuredSpace), Filter.Tendsto (fun (n : ℕ) => toRootedMeasuredGHSpace (X n)) Filter.atTop (nhds (toRootedMeasuredGHSpace Y))

Geometrically small actual rooted coupling costs yield a rooted compact measured limit. The probability and the limiting root both live on the full Hausdorff-limit carrier.

instance BGW.MetricMeasure.RootedMeasuredGHSpace.instCompleteSpace : CompleteSpace RootedMeasuredGHSpace

The existing whole-carrier rooted GHP metric is complete.

theorem BGW.MetricMeasure.RootedMeasuredGHSpace.polishSpace : PolishSpace RootedMeasuredGHSpace

The existing rooted GHP metric topology is Polish.