Positive spatial scaling of unrooted measured GH classes

The same representative scaling used for rooted compact probability spaces descends to the unrooted whole-carrier measured-isometry quotient. Measure transport is unchanged. As in the rooted case, GHP estimates use max factor 1 because the Lévy–Prokhorov component is not homogeneous under spatial scaling.

theorem BGW.MetricMeasure.CompactMeasuredSpace.measuredIsometry_scale (factor : ℝ) (hfactor : 0 < factor) {X Y : CompactMeasuredSpace} (h : X.MeasuredIsometry Y) : (scale factor hfactor X).MeasuredIsometry (scale factor hfactor Y)

Whole-carrier measured isometries remain so after positive spatial scaling.

theorem BGW.MetricMeasure.CompactMeasuredSpace.distance_scale_le (factor : ℝ) (hfactor : 0 < factor) (X Y : CompactMeasuredSpace) : (scale factor hfactor X).distance (scale factor hfactor Y) ≤ max factor 1 * X.distance Y

Positive scaling is Lipschitz for the represented unrooted GHP distance.

theorem BGW.MetricMeasure.CompactMeasuredSpace.measuredIsometry_scale_one (X : CompactMeasuredSpace) : (scale 1 ⋯ X).MeasuredIsometry X

Scaling by one preserves the represented unrooted measured isometry class.

theorem BGW.MetricMeasure.CompactMeasuredSpace.measuredIsometry_scale_inv (factor : ℝ) (hfactor : 0 < factor) (X : CompactMeasuredSpace) : (scale factor⁻¹ ⋯ (scale factor hfactor X)).MeasuredIsometry X

Scaling by the positive reciprocal cancels the first scaling, including the measure.

theorem BGW.MetricMeasure.CompactMeasuredSpace.min_mul_distance_le_scale (factor : ℝ) (hfactor : 0 < factor) (X Y : CompactMeasuredSpace) : min factor 1 * X.distance Y ≤ (scale factor hfactor X).distance (scale factor hfactor Y)

The inverse scaling gives the lower bound with factor min factor 1.

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

Changing the positive scaling factor is controlled by the representative diameter.

noncomputable def BGW.MetricMeasure.MeasuredGHSpace.scale (factor : ℝ) (hfactor : 0 < factor) : MeasuredGHSpace → MeasuredGHSpace

Positive spatial scaling on whole-carrier unrooted measured isometry classes.

Equations

• BGW.MetricMeasure.MeasuredGHSpace.scale factor hfactor = Quotient.map (BGW.MetricMeasure.CompactMeasuredSpace.scale factor hfactor) ⋯

@[simp]

theorem BGW.MetricMeasure.MeasuredGHSpace.scale_toMeasuredGHSpace (factor : ℝ) (hfactor : 0 < factor) (X : CompactMeasuredSpace) : scale factor hfactor (toMeasuredGHSpace X) = toMeasuredGHSpace (CompactMeasuredSpace.scale factor hfactor X)

Scaling a quotient class is scaling any of its compact measured representatives.

@[simp]

theorem BGW.MetricMeasure.MeasuredGHSpace.scale_one (X : MeasuredGHSpace) : scale 1 ⋯ X = X

Scaling an unrooted measured GH class by one is the identity.

@[simp]

theorem BGW.MetricMeasure.MeasuredGHSpace.scale_inv (factor : ℝ) (hfactor : 0 < factor) (X : MeasuredGHSpace) : scale factor⁻¹ ⋯ (scale factor hfactor X) = X

Scaling by a positive factor and its reciprocal is the identity on unrooted measured classes.

theorem BGW.MetricMeasure.MeasuredGHSpace.dist_scale_le (factor : ℝ) (hfactor : 0 < factor) (X Y : MeasuredGHSpace) : dist (scale factor hfactor X) (scale factor hfactor Y) ≤ max factor 1 * dist X Y

Positive spatial scaling has the same upper GHP Lipschitz bound as in the rooted case.

theorem BGW.MetricMeasure.MeasuredGHSpace.min_mul_dist_le_scale (factor : ℝ) (hfactor : 0 < factor) (X Y : MeasuredGHSpace) : min factor 1 * dist X Y ≤ dist (scale factor hfactor X) (scale factor hfactor Y)

Positive spatial scaling has the lower GHP expansion bound min factor 1.

theorem BGW.MetricMeasure.MeasuredGHSpace.lipschitzWith_scale (factor : ℝ) (hfactor : 0 < factor) : LipschitzWith ⟨max factor 1, ⋯⟩ (scale factor hfactor)

Fixed-factor spatial scaling is Lipschitz for the unrooted measured GHP metric.

theorem BGW.MetricMeasure.MeasuredGHSpace.continuous_scale (factor : ℝ) (hfactor : 0 < factor) : Continuous (scale factor hfactor)

Fixed-factor spatial scaling is continuous on unrooted measured GH classes.

theorem BGW.MetricMeasure.MeasuredGHSpace.measurable_scale (factor : ℝ) (hfactor : 0 < factor) : Measurable (scale factor hfactor)

Fixed-factor spatial scaling is Borel measurable on unrooted measured GH classes.

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

Spatial scaling is jointly continuous in its positive factor and unrooted measured class.

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

Joint spatial scaling is Borel measurable for the product Borel structure.