The continuous underlying GH projection

Forgetting the measure is well-defined on the source whole-space measured isometry classes. The actual GH≤GHP inequality makes this projection nonexpansive, so it is continuous and Borel measurable. No assumption about Polishness or the Gromov--Prokhorov quotient is needed.

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

noncomputable def BGW.MetricMeasure.MeasuredGHSpace.underlyingGH : MeasuredGHSpace → GromovHausdorff.GHSpace

Forget the measure while retaining the entire underlying compact space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGW.MetricMeasure.MeasuredGHSpace.underlyingGH_toMeasuredGHSpace (X : CompactMeasuredSpace) : (toMeasuredGHSpace X).underlyingGH = GromovHausdorff.toGHSpace X.carrier

theorem BGW.MetricMeasure.MeasuredGHSpace.lipschitzWith_underlyingGH : LipschitzWith 1 underlyingGH

The source's underlying-space projection cannot increase distances.

theorem BGW.MetricMeasure.MeasuredGHSpace.continuous_underlyingGH : Continuous underlyingGH

theorem BGW.MetricMeasure.MeasuredGHSpace.measurable_underlyingGH : Measurable underlyingGH

With the usual Borel structure on GHSpace, the source projection is measurable as asserted in the topology appendix.