Finite atom bounds for Prokhorov distance

The difference on any event is bounded by the sum of the absolute differences of its atomic masses. This gives a Prokhorov bound without a lower bound on nonzero masses or on distances between points. Quantizing each atom at a scale divided by the number of points yields countable approximation data.

Adapted from Freezing2/Probability/FiniteProkhorov.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

theorem BGW.MetricMeasure.abs_measureReal_sub_le_sum_atoms {X : Type u_1} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (B : Set X) : |μ.real B - ν.real B| ≤ ∑ x : X, |μ.real {x} - ν.real {x}|

Atomic mass discrepancies bound the discrepancy on every event.

theorem BGW.MetricMeasure.levyProkhorovDist_le_sum_atoms {X : Type u_1} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [MetricSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.levyProkhorovDist μ ν ≤ ∑ x : X, |μ.real {x} - ν.real {x}|

On a finite metric space, the genuine Prokhorov distance is at most the sum of absolute atomic mass discrepancies. No full-support premise is used.

theorem BGW.MetricMeasure.abs_sub_le_of_floor_div_eq {a b η : ℝ} (hη : 0 < η) (h : ⌊a / η⌋ = ⌊b / η⌋) : |a - b| ≤ η

Equality of integer parts at scale η bounds the unscaled discrepancy.

theorem BGW.MetricMeasure.levyProkhorovDist_le_card_mul_of_floor_atoms_eq {X : Type u_1} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [MetricSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {η : ℝ} (hη : 0 < η) (hcode : ∀ (x : X), ⌊μ.real {x} / η⌋ = ⌊ν.real {x} / η⌋) : MeasureTheory.levyProkhorovDist μ ν ≤ ↑(Fintype.card X) * η

Equal rounded atomic masses give an error proportional to the number of points. All atoms, including zero-mass atoms, are part of the code.

noncomputable def BGW.MetricMeasure.finiteWeightCode {X : Type u_1} [Fintype X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) (ε : ℝ) : X → ℤ

The finite weight code uses a mesh of ε / card X, so equal codes are within ε independently of the number of finite points.

Equations

• BGW.MetricMeasure.finiteWeightCode μ ε x = ⌊μ.real {x} / (ε / ↑(Fintype.card X))⌋

theorem BGW.MetricMeasure.levyProkhorovDist_le_of_finiteWeightCode_eq {X : Type u_1} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [Nonempty X] [MetricSpace X] [BorelSpace X] (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {ε : ℝ} (hε : 0 < ε) (hcode : finiteWeightCode μ ε = finiteWeightCode ν ε) : MeasureTheory.levyProkhorovDist μ ν ≤ ε