GHP continuity of the actual finite iid distance-matrix laws #
The compactness extraction is retained together with its fixed compact ambient sampling measures. Their weak convergence gives every finite matrix law by product continuity. For a GHP-convergent sequence, uniqueness identifies every subsequential limit, giving continuity of the quotient observable. Neither distinct samples nor full measure support is assumed.
Adapted from Freezing2/Probability/SampledDistanceContinuity.lean in
igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit
8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).
Every finite iid sampled-distance law is continuous for the exact source GHP topology on whole-space measured-isometry classes.
The finite sampled-distance observables are Borel measurable.