Finite measured approximations in the exact GHP distance

A finite cover of the entire compact carrier gives a measurable finite-valued map by testing its balls one at a time. Its pushforward supplies the finite weights; no support or positivity condition on those weights is imposed. The common ambient space is the original carrier, and both the Hausdorff and Prokhorov contributions are bounded by the covering radius.

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

theorem BGW.MetricMeasure.exists_measurable_finite_ball_selector {X : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] (s : Finset X) (a : X) (ε : ℝ) : ∃ (f : X → X), Measurable f ∧ ∀ (x : X), (∃ y ∈ s, dist x y < ε) → f x ∈ s ∧ dist x (f x) < ε

Finite ball tests give a measurable choice on the part covered by a finite set. Outside the cover the default value is immaterial.

theorem BGW.MetricMeasure.exists_measurable_net_projection {X : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] (s : Finset X) {ε : ℝ} (hcover : ∀ (x : X), ∃ y ∈ s, dist x y < ε) : ∃ (q : X → ↥s), Measurable q ∧ ∀ (x : X), dist x ↑(q x) < ε

A measurable choice of a covering center, constructed by finitely many measurable tests rather than by an assumed selection principle.

theorem BGW.MetricMeasure.exists_finite_measurable_net {X : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] [CompactSpace X] {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset X), s.Nonempty ∧ ∃ (q : X → ↥s), Measurable q ∧ ∀ (x : X), dist x ↑(q x) < ε

Every nonempty compact carrier has a nonempty finite net and a measurable projection to it. The coverage statement includes points of zero measure.

theorem BGW.MetricMeasure.ghpDistance_finite_projection_le {X : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (s : Finset X) (q : X → ↥s) (hq : Measurable q) {ε : ℝ} (hε : 0 ≤ ε) (hclose : ∀ (x : X), dist x ↑(q x) ≤ ε) : ghpDistance μ (MeasureTheory.Measure.map q μ) ≤ 2 * ε

The exact pushforward to a finite net approximates the original probability measure in the manuscript's summed GHP distance. Centers of zero pushforward mass are retained in the finite metric space.

theorem BGW.MetricMeasure.exists_finite_ghp_approximation {X : Type u} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] [CompactSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset X), s.Nonempty ∧ ∃ (q : X → ↥s), Measurable q ∧ MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map q μ) ∧ (∀ (x : X), dist x ↑(q x) < ε) ∧ ghpDistance μ (MeasureTheory.Measure.map q μ) ≤ 2 * ε

Finite measured spaces are dense for the exact GHP distance, with the measure given explicitly by the measurable projection's pushforward.