Spatial scaling of continuously coded trees

Multiplying a coding function by a nonnegative constant multiplies its pseudodistance by that constant. For a positive constant, this identifies the coded tree with the spatially scaled original tree by a genuine isometry preserving the root and the Lebesgue pushforward mass.

This is an identity between scaled spaces. It does not assert homogeneity of GHP distance between two spaces, whose Prokhorov term also measures mass error.

theorem BGW.ContinuumTrees.Coding.intervalMin_smul (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 ≤ factor) (s t : ↑unitInterval) : intervalMin (factor • g) s t = factor * intervalMin g s t

Nonnegative multiplication commutes with the attained interval minimum.

theorem BGW.ContinuumTrees.Coding.codingDist_smul (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 ≤ factor) (s t : ↑unitInterval) : codingDist (factor • g) s t = factor * codingDist g s t

The coding pseudodistance is homogeneous under nonnegative multiplication.

noncomputable def BGW.ContinuumTrees.Coding.scalingMap (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 ≤ factor) : Space g → Space (factor • g)

The map between coding quotients represented by keeping the same time.

Equations

• BGW.ContinuumTrees.Coding.scalingMap g factor hf = SeparationQuotient.lift (fun (x : BGW.ContinuumTrees.Coding.Point g) => BGW.ContinuumTrees.Coding.projection (factor • g) x.time) ⋯

@[simp]

theorem BGW.ContinuumTrees.Coding.scalingMap_projection (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 ≤ factor) (t : ↑unitInterval) : scalingMap g factor hf (projection g t) = projection (factor • g) t

theorem BGW.ContinuumTrees.Coding.dist_scalingMap (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 ≤ factor) (x y : Space g) : dist (scalingMap g factor hf x) (scalingMap g factor hf y) = factor * dist x y

theorem BGW.ContinuumTrees.Coding.scalingMap_surjective (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 ≤ factor) : Function.Surjective (scalingMap g factor hf)

theorem BGW.ContinuumTrees.Coding.isometry_scalingMap_ofScaled (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 < factor) : Isometry fun (x : MetricMeasure.ScaledMetric ⟨factor, hf⟩ (Space g)) => scalingMap g factor ⋯ (MetricMeasure.ScaledMetric.ofScaled ⟨factor, hf⟩ x)

The same-time map is an isometry when its source carries the positively scaled metric.

noncomputable def BGW.ContinuumTrees.Coding.scalingIsometry (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 < factor) : MetricMeasure.ScaledMetric ⟨factor, hf⟩ (Space g) ≃ᵢ Space (factor • g)

The spatially scaled coded tree is isometric to the tree coded by the scaled function.

Equations

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

@[simp]

theorem BGW.ContinuumTrees.Coding.scalingIsometry_projection (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 < factor) (t : ↑unitInterval) : (scalingIsometry g factor hf) (MetricMeasure.ScaledMetric.toScaled ⟨factor, hf⟩ (projection g t)) = projection (factor • g) t

theorem BGW.ContinuumTrees.Coding.map_mass_scalingIsometry (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 < factor) : MeasureTheory.Measure.map (⇑(scalingIsometry g factor hf)) (MeasureTheory.Measure.map (MetricMeasure.ScaledMetric.toScaled ⟨factor, hf⟩) ↑(mass g)) = ↑(mass (factor • g))

The natural isometry preserves the actual Lebesgue pushforward mass.

theorem BGW.ContinuumTrees.Coding.measuredIsometry_scaling (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 < factor) : (MetricMeasure.RootedCompactMeasuredSpace.scale factor hf (rootedCompactMeasuredSpace g)).MeasuredIsometry (rootedCompactMeasuredSpace (factor • g))

Scaling the function scales the entire rooted measured tree, without changing mass.

theorem BGW.ContinuumTrees.Coding.rootedMeasuredGHSpace_smul (g : C(↑unitInterval, ℝ)) (factor : ℝ) (hf : 0 < factor) : MetricMeasure.RootedMeasuredGHSpace.scale factor hf (rootedMeasuredGHSpace g) = rootedMeasuredGHSpace (factor • g)

Equality of the corresponding rooted measured isometry classes.