Countable data for finite measured metric spaces

A labelled finite carrier is encoded by rounded pairwise distances and rounded atomic masses. Equal codes give a measure comparison and a bijection of small distortion, hence a bound for the exact GHP distance. Zero-mass points are included in both arrays.

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

noncomputable def BGW.MetricMeasure.finiteMeasuredCode {X : Type u} [MetricSpace X] [MeasurableSpace X] {n : ℕ} (μ : MeasureTheory.Measure X) (e : X ≃ Fin n) (ε : ℝ) : (Fin n → Fin n → ℤ) × (Fin n → ℤ)

Distance and weight arrays of a finite labelled measured space.

Equations

• BGW.MetricMeasure.finiteMeasuredCode μ e ε = (fun (i j : Fin n) => ⌊dist (e.symm i) (e.symm j) / ε⌋, fun (i : Fin n) => ⌊μ.real {e.symm i} / (ε / ↑n)⌋)

theorem BGW.MetricMeasure.ghpDistance_le_of_finiteMeasuredCode_eq {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [Fintype X] [Fintype Y] [Nonempty X] [Nonempty Y] [BorelSpace X] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {n : ℕ} (e : X ≃ Fin n) (f : Y ≃ Fin n) {ε : ℝ} (hε : 0 < ε) (hcode : finiteMeasuredCode μ e ε = finiteMeasuredCode ν f ε) : ghpDistance μ ν ≤ 3 * ε

Coinciding finite codes control the exact summed GHP infimum.

theorem BGW.MetricMeasure.ghpDistance_le_of_sigma_finiteMeasuredCode_eq {X Y : Type u} [MetricSpace X] [MeasurableSpace X] [MetricSpace Y] [MeasurableSpace Y] [Fintype X] [Fintype Y] [Nonempty X] [Nonempty Y] [BorelSpace X] [BorelSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {n m : ℕ} (e : X ≃ Fin n) (f : Y ≃ Fin m) {ε : ℝ} (hε : 0 < ε) (hcode : ⟨n, finiteMeasuredCode μ e ε⟩ = ⟨m, finiteMeasuredCode ν f ε⟩) : ghpDistance μ ν ≤ 3 * ε

The same comparison for dependent codes whose first entry records the number of points. Equality of the cardinality entries is derived from the code equality, so the caller need not identify the two index types first.