Positive rescaling of a metric carrier

ScaledMetric c X is a fresh carrier with distance multiplied by the positive number c. Its topology and measurable structure are transported from X. MetricSpace.ofDistTopology makes the metric induce that very topology. No metric instance on the original carrier is changed.

The two quantitative helpers control Hausdorff distance on compact sets and Lévy–Prokhorov distance under Lipschitz maps. The latter uses the factor max K 1, since the probability-error term is not spatially rescaled.

def BGW.MetricMeasure.ScaledMetric (_c : ↑(Set.Ioi 0)) (X : Type u) : Type u

A carrier whose distances are multiplied by one fixed positive real number.

Equations

• BGW.MetricMeasure.ScaledMetric _c X = X

def BGW.MetricMeasure.ScaledMetric.toScaled (c : ↑(Set.Ioi 0)) {X : Type u} (x : X) : ScaledMetric c X

View a point in the carrier whose distances are scaled by c.

Equations

• BGW.MetricMeasure.ScaledMetric.toScaled c x = x

def BGW.MetricMeasure.ScaledMetric.ofScaled (c : ↑(Set.Ioi 0)) {X : Type u} (x : ScaledMetric c X) : X

Recover the original point from the scaled carrier.

Equations

• BGW.MetricMeasure.ScaledMetric.ofScaled c x = x

@[simp]

theorem BGW.MetricMeasure.ScaledMetric.ofScaled_toScaled (c : ↑(Set.Ioi 0)) {X : Type u} (x : X) : ofScaled c (toScaled c x) = x

@[simp]

theorem BGW.MetricMeasure.ScaledMetric.toScaled_ofScaled (c : ↑(Set.Ioi 0)) {X : Type u} (x : ScaledMetric c X) : toScaled c (ofScaled c x) = x

def BGW.MetricMeasure.ScaledMetric.equiv (c : ↑(Set.Ioi 0)) (X : Type u) : X ≃ ScaledMetric c X

The identity bijection between the original and scaled carriers.

Equations

• BGW.MetricMeasure.ScaledMetric.equiv c X = { toFun := BGW.MetricMeasure.ScaledMetric.toScaled c, invFun := BGW.MetricMeasure.ScaledMetric.ofScaled c, left_inv := ⋯, right_inv := ⋯ }

instance BGW.MetricMeasure.ScaledMetric.instNonempty (c : ↑(Set.Ioi 0)) {X : Type u} [Nonempty X] : Nonempty (ScaledMetric c X)

@[instance_reducible]

instance BGW.MetricMeasure.ScaledMetric.instTopologicalSpace (c : ↑(Set.Ioi 0)) {X : Type u} [TopologicalSpace X] : TopologicalSpace (ScaledMetric c X)

Equations

• BGW.MetricMeasure.ScaledMetric.instTopologicalSpace c = BGW.MetricMeasure.ScaledMetric.instTopologicalSpace._aux_1 c

@[instance_reducible]

instance BGW.MetricMeasure.ScaledMetric.instMeasurableSpace (c : ↑(Set.Ioi 0)) {X : Type u} [MeasurableSpace X] : MeasurableSpace (ScaledMetric c X)

Equations

• BGW.MetricMeasure.ScaledMetric.instMeasurableSpace c = BGW.MetricMeasure.ScaledMetric.instMeasurableSpace._aux_1 c

instance BGW.MetricMeasure.ScaledMetric.instCompactSpace (c : ↑(Set.Ioi 0)) {X : Type u} [TopologicalSpace X] [CompactSpace X] : CompactSpace (ScaledMetric c X)

instance BGW.MetricMeasure.ScaledMetric.instBorelSpace (c : ↑(Set.Ioi 0)) {X : Type u} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] : BorelSpace (ScaledMetric c X)

theorem BGW.MetricMeasure.ScaledMetric.continuous_toScaled (c : ↑(Set.Ioi 0)) {X : Type u} [TopologicalSpace X] : Continuous (toScaled c)

theorem BGW.MetricMeasure.ScaledMetric.continuous_ofScaled (c : ↑(Set.Ioi 0)) {X : Type u} [TopologicalSpace X] : Continuous (ofScaled c)

theorem BGW.MetricMeasure.ScaledMetric.measurable_toScaled (c : ↑(Set.Ioi 0)) {X : Type u} [MeasurableSpace X] : Measurable (toScaled c)

theorem BGW.MetricMeasure.ScaledMetric.measurable_ofScaled (c : ↑(Set.Ioi 0)) {X : Type u} [MeasurableSpace X] : Measurable (ofScaled c)

def BGW.MetricMeasure.ScaledMetric.homeomorph (c : ↑(Set.Ioi 0)) {X : Type u} [TopologicalSpace X] : X ≃ₜ ScaledMetric c X

The identity homeomorphism for the topology retained by the scaled carrier.

Equations

• BGW.MetricMeasure.ScaledMetric.homeomorph c = { toEquiv := BGW.MetricMeasure.ScaledMetric.equiv c X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[instance_reducible]

instance BGW.MetricMeasure.ScaledMetric.instMetricSpace (c : ↑(Set.Ioi 0)) {X : Type u} [MetricSpace X] : MetricSpace (ScaledMetric c X)

Equations

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

@[simp]

theorem BGW.MetricMeasure.ScaledMetric.dist_toScaled (c : ↑(Set.Ioi 0)) {X : Type u} [MetricSpace X] (x y : X) : dist (toScaled c x) (toScaled c y) = ↑c * dist x y

theorem BGW.MetricMeasure.ScaledMetric.lipschitzWith_toScaled (c : ↑(Set.Ioi 0)) {X : Type u} [MetricSpace X] : LipschitzWith ⟨↑c, ⋯⟩ (toScaled c)

theorem BGW.MetricMeasure.ScaledMetric.map_ofScaled_map_toScaled (c : ↑(Set.Ioi 0)) {X : Type u} [MeasurableSpace X] (μ : MeasureTheory.Measure X) : MeasureTheory.Measure.map (ofScaled c) (MeasureTheory.Measure.map (toScaled c) μ) = μ

theorem BGW.MetricMeasure.ScaledMetric.map_toScaled_univ (c : ↑(Set.Ioi 0)) {X : Type u} [MeasurableSpace X] (μ : MeasureTheory.Measure X) : (MeasureTheory.Measure.map (toScaled c) μ) Set.univ = μ Set.univ

theorem BGW.MetricMeasure.levyProkhorovDist_map_le_mul {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {K : NNReal} {f : X → Y} (hf : LipschitzWith K f) : MeasureTheory.levyProkhorovDist (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) ≤ max (↑K) 1 * MeasureTheory.levyProkhorovDist μ ν

A Lipschitz map controls the Prokhorov radius and the unchanged mass-error term.

theorem BGW.MetricMeasure.hausdorffDist_image_le_mul_of_lipschitz {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {K : NNReal} {f : X → Y} (hf : LipschitzWith K f) {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hsne : s.Nonempty) (htne : t.Nonempty) : Metric.hausdorffDist (f '' s) (f '' t) ≤ ↑K * Metric.hausdorffDist s t

A Lipschitz map controls Hausdorff distance between nonempty compact sets.