The genuine GHP metric on whole-space measured isometry classes #
The already constructed quotient and its topology are unchanged. Zero exact GHP distance forces a measure-preserving isometry, so the existing pseudometric is a metric. Completeness and separability remain separate.
Adapted from Freezing2/Geometry/MeasuredGHMetric.lean in
igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit
8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).
@[instance_reducible]
Separation upgrades the exact existing quotient pseudometric. Its distance, uniformity, topology and Borel structure are preserved definitionally.
Equations
- One or more equations did not get rendered due to their size.