Compactness transfer from GH to GHP

Hausdorff-precompact full carriers can be put in a common compact hull. Probability compactness on that hull gives a measured convergent subsequence, regardless of the original measures. The limit retains the entire Hausdorff carrier. Consequently the inverse image of a compact GH set under the underlying-space projection is compact for the exact GHP metric.

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

theorem BGW.MetricMeasure.exists_measured_subsequence_of_common_ambient (X : ℕ → CompactMeasuredSpace) {Z : Type u} [MetricSpace Z] [MeasurableSpace Z] [BorelSpace Z] [CompleteSpace Z] (ι : (n : ℕ) → (X n).carrier → Z) (hι : ∀ (n : ℕ), Isometry (ι n)) (S : ℕ → TopologicalSpace.NonemptyCompacts Z) (hS : ∀ (n : ℕ), ↑(S n) = Set.range (ι n)) (hcS : CauchySeq S) : ∃ (Y : CompactMeasuredSpace) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto ((fun (n : ℕ) => toMeasuredGHSpace (X n)) ∘ φ) Filter.atTop (nhds (toMeasuredGHSpace Y))

Hausdorff-Cauchy full carrier images in a complete common ambient space have a GHP-convergent measured subsequence. The measures need not be Cauchy.

theorem BGW.MetricMeasure.exists_measured_subsequence_of_gh_cauchy (X : ℕ → CompactMeasuredSpace) (hc : CauchySeq fun (n : ℕ) => GromovHausdorff.toGHSpace (X n).carrier) : ∃ (Y : CompactMeasuredSpace) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto ((fun (n : ℕ) => toMeasuredGHSpace (X n)) ∘ φ) Filter.atTop (nhds (toMeasuredGHSpace Y))

GH-Cauchy underlying carriers admit a GHP-convergent subsequence for arbitrary Borel probability measures on their entire carriers.

theorem BGW.MetricMeasure.MeasuredGHSpace.isCompact_preimage_underlyingGH {A : Set GromovHausdorff.GHSpace} (hA : IsCompact A) : IsCompact (underlyingGH ⁻¹' A)

Forgetting the measure has compact inverse images of compact GH sets. No uniform lower bound on masses, or full-support hypothesis, is imposed.