Represented rooted compact metric probability spaces

The bundle adds just a point to the existing compact measured space. The root may lie outside the measure support. The represented distance is the actual ambient rooted GHP infimum. No quotient or metric-space instance on represented spaces is introduced here.

structure BGW.MetricMeasure.RootedCompactMeasuredSpace : Type (u + 1)

A compact metric probability space together with one distinguished point.

• space : CompactMeasuredSpace

  The underlying compact metric probability space.

• root : self.space.carrier

  The distinguished point of the whole carrier, with no support requirement.

noncomputable def BGW.MetricMeasure.RootedCompactMeasuredSpace.distance (X Y : RootedCompactMeasuredSpace) : ℝ

Root distance plus Hausdorff and Lévy–Prokhorov costs, minimized over common realizations.

Equations

• X.distance Y = BGW.MetricMeasure.rootedGHPDistance (↑X.space.law) (↑Y.space.law) X.root Y.root

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_nonneg (X Y : RootedCompactMeasuredSpace) : 0 ≤ X.distance Y

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_comm (X Y : RootedCompactMeasuredSpace) : X.distance Y = Y.distance X

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_self (X : RootedCompactMeasuredSpace) : X.distance X = 0

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_triangle (X Y Z : RootedCompactMeasuredSpace) : X.distance Z ≤ X.distance Y + Y.distance Z

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_space_le (X Y : RootedCompactMeasuredSpace) : X.space.distance Y.space ≤ X.distance Y

Forgetting the distinguished point does not increase distance.