Positive spatial scaling of rooted compact probability spaces

Only distances are multiplied by the positive factor. Probability measures and roots are transported by the canonical equivalence to ScaledMetric. The GHP comparison uses max factor 1; the probability-error part of the Lévy–Prokhorov metric is not homogeneous under spatial scaling.

def BGW.MetricMeasure.ScaledMetric.map (c : ↑(Set.Ioi 0)) {X Y : Type u} (f : X → Y) : ScaledMetric c X → ScaledMetric c Y

Transport a map to the two scaled carriers.

Equations

• BGW.MetricMeasure.ScaledMetric.map c f x = BGW.MetricMeasure.ScaledMetric.toScaled c (f (BGW.MetricMeasure.ScaledMetric.ofScaled c x))

@[simp]

theorem BGW.MetricMeasure.ScaledMetric.map_toScaled (c : ↑(Set.Ioi 0)) {X Y : Type u} (f : X → Y) (x : X) : map c f (toScaled c x) = toScaled c (f x)

theorem BGW.MetricMeasure.ScaledMetric.measurable_map (c : ↑(Set.Ioi 0)) {X Y : Type u} [MeasurableSpace X] [MeasurableSpace Y] {f : X → Y} (hf : Measurable f) : Measurable (map c f)

theorem BGW.MetricMeasure.ScaledMetric.isometry_map (c : ↑(Set.Ioi 0)) {X Y : Type u} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Isometry f) : Isometry (map c f)

def BGW.MetricMeasure.ScaledMetric.isometryEquiv (c : ↑(Set.Ioi 0)) {X Y : Type u} [MetricSpace X] [MetricSpace Y] (e : X ≃ᵢ Y) : ScaledMetric c X ≃ᵢ ScaledMetric c Y

An isometry equivalence transports to the scaled carriers.

Equations

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

@[simp]

theorem BGW.MetricMeasure.ScaledMetric.isometryEquiv_toScaled (c : ↑(Set.Ioi 0)) {X Y : Type u} [MetricSpace X] [MetricSpace Y] (e : X ≃ᵢ Y) (x : X) : (isometryEquiv c e) (toScaled c x) = toScaled c (e x)

theorem BGW.MetricMeasure.ScaledMetric.map_measure_toScaled (c : ↑(Set.Ioi 0)) {X Y : Type u} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) {f : X → Y} (hf : Measurable f) : MeasureTheory.Measure.map (map c f) (MeasureTheory.Measure.map (toScaled c) μ) = MeasureTheory.Measure.map (toScaled c) (MeasureTheory.Measure.map f μ)

theorem BGW.MetricMeasure.ScaledMetric.range_map (c : ↑(Set.Ioi 0)) {X Y : Type u} (f : X → Y) : Set.range (map c f) = toScaled c '' Set.range f

noncomputable def BGW.MetricMeasure.CompactMeasuredSpace.scale (factor : ℝ) (hfactor : 0 < factor) (X : CompactMeasuredSpace) : CompactMeasuredSpace

Multiply distances by factor > 0, transporting the unchanged probability measure.

Equations

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

noncomputable def BGW.MetricMeasure.RootedCompactMeasuredSpace.scale (factor : ℝ) (hfactor : 0 < factor) (X : RootedCompactMeasuredSpace) : RootedCompactMeasuredSpace

Positive spatial scaling, with the distinguished point transported to the new carrier.

Equations

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

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

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

def BGW.MetricMeasure.GHPCoupling.scale {X Y : Type u} [MetricSpace X] [MetricSpace Y] (c : ↑(Set.Ioi 0)) (C : GHPCoupling X Y) : GHPCoupling (ScaledMetric c X) (ScaledMetric c Y)

Scale the two carriers and the actual common ambient realization by the same factor.

Equations

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

theorem BGW.MetricMeasure.GHPCoupling.rootedCost_scale_le {X Y : Type u} [MetricSpace X] [MetricSpace Y] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] (c : ↑(Set.Ioi 0)) (C : GHPCoupling X Y) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (x : X) (y : Y) : (scale c C).rootedCost (MeasureTheory.Measure.map (ScaledMetric.toScaled c) μ) (MeasureTheory.Measure.map (ScaledMetric.toScaled c) ν) (ScaledMetric.toScaled c x) (ScaledMetric.toScaled c y) ≤ max (↑c) 1 * C.rootedCost μ ν x y

Each scaled ambient cost is at most max c 1 times its original rooted cost.

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

Positive scaling is Lipschitz for the represented rooted GHP distance.

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

Scaling by one preserves the represented rooted measured isometry class.

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

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

theorem BGW.MetricMeasure.RootedCompactMeasuredSpace.min_mul_distance_le_scale (factor : ℝ) (hfactor : 0 < factor) (X Y : RootedCompactMeasuredSpace) : 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.

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

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

Equations

• BGW.MetricMeasure.RootedMeasuredGHSpace.scale factor hfactor = Quotient.map (BGW.MetricMeasure.RootedCompactMeasuredSpace.scale factor hfactor) ⋯

@[simp]

theorem BGW.MetricMeasure.RootedMeasuredGHSpace.scale_toRootedMeasuredGHSpace (factor : ℝ) (hfactor : 0 < factor) (X : RootedCompactMeasuredSpace) : scale factor hfactor (toRootedMeasuredGHSpace X) = toRootedMeasuredGHSpace (RootedCompactMeasuredSpace.scale factor hfactor X)

@[simp]

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

@[simp]

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

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

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

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

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

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