Joint continuity of positive spatial scaling

Two positive scalings of one represented compact probability space are compared using their common original carrier and probability law. The distortion is the difference of factors times the original diameter. The common-source gluing estimate therefore gives the rooted GHP bound with constant 3 / 2.

Combining this estimate with the fixed-factor Lipschitz bound proves joint continuity on positive factors and rooted measured isometry classes. The argument fixes a representative only at the point of continuity; it does not introduce a global choice of representatives or a diameter observable on the quotient. Probability masses are unchanged throughout.

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.distance_scale_scale_le (c d : ℝ) (hc : 0 < c) (hd : 0 < d) (X : RootedCompactMeasuredSpace) : (scale c hc X).distance (scale d hd X) ≤ 3 / 2 * |c - d| * Metric.diam Set.univ

Changing the scaling factor on one represented space is controlled by its diameter.

theorem BGW.MetricMeasure.RootedMeasuredGHSpace.continuous_scale_joint : Continuous fun (p : ↑(Set.Ioi 0) × RootedMeasuredGHSpace) => scale ↑p.1 ⋯ p.2

Spatial scaling is continuous jointly in the positive factor and the rooted measured space.

theorem BGW.MetricMeasure.RootedMeasuredGHSpace.measurable_scale_joint : Measurable fun (p : ↑(Set.Ioi 0) × RootedMeasuredGHSpace) => scale ↑p.1 ⋯ p.2

Joint measurability uses the second countability of the positive real factor.