Approximation of a finite-moment law by a finitely supported one

On a separable ground space every probability measure with finite p-moment can be pushed within any prescribed Wasserstein accuracy by a quantizer, for every finite exponent 1 ≤ p < ∞. When singletons are measurable, these pushforwards are measures carried by finite sets. This file also records the two standard consequences: the finitely supported laws are dense in TauCeti.WassersteinSpace p X under the compatible standard-Borel and second-countability hypotheses, and the N-point quantization error of a fixed law tends to 0.

The approximating measures are produced by a quantizer: a measurable map T : X → X with finitely many values, approximating the identity. The displacement bound TauCeti.wassersteinEDist_map_le — the graph plan of T is a coupling of μ with μ.map T, so the Wasserstein distance between them is at most the L^p (μ) seminorm of x ↦ edist x (T x) — turns an estimate on the displacement into an estimate on the distance. The map itself sends x to u i, for the least index i of a dense sequence u with dist x (u i) < δ when that index is smaller than a cutoff n, and to u 0 otherwise. The displacement is then at most δ off the tail set of points whose least index is at least n, and those tail sets decrease to the empty set, so, the finite p-moment about u 0 making μ.withDensity (edist (u 0) · ^ p) a finite measure, their contribution vanishes by continuity of measure from above.

This file also provides the finite-support transport estimate and the approximation of a finitely supported law by one whose weights have a common natural denominator, the rounding of the weights themselves being TauCeti.exists_nat_weights_of_sum_eq_one, together with the companion quantization onto the terms of a prescribed dense sequence, which sends a point to the first term of the sequence within the prescribed accuracy of it.

The construction uses a finite exponent: at p = ∞ a displacement that is small off a set of small measure is not small in L^∞, and finitely supported laws need not be W_∞-dense on a general separable metric space (for example, on a countably infinite discrete metric space). The ground space is separable, which is where the dense sequence comes from.

Support conventions

A quantizer statement — the map T takes finitely many values — is available on a pseudometric ground space, whereas the assertion that a measure gives mass 0 to the complement of a finite set is not: in a pseudometric space that complement need not be measurable. On an infinite type with the zero pseudometric and its Borel structure, no probability measure vanishes on the complement of a finite set. The measure-level statements therefore ask for measurable singletons, which a metric ground space with its Borel structure supplies for free. For the same reason the finite carrier is recorded as a Finset X whose complement is null, rather than through MeasureTheory.Measure.support: on a pseudometric space the topological support of a Dirac law is the whole ball of radius 0 around its atom, so it is not finite.

Main statements

• TauCeti.wassersteinEDist_map_le — the displacement bound: W_p (μ, T_* μ) is at most the L^p (μ) seminorm of x ↦ edist x (T x);
• TauCeti.hasFiniteMoment_of_ae_mem_finset — a law carried by a finite set has finite p-moment for every exponent;
• TauCeti.wassersteinEDist_sum_smul_dirac_le — a transport bound for perturbing the weights of a finitely supported law;
• TauCeti.exists_nat_weights_wassersteinEDist_le — approximation by weights with a common natural denominator;
• TauCeti.exists_map_range_wassersteinEDist_le — quantization onto a dense sequence: some measurable map with values among the terms of a dense sequence pushes ν to within δ of itself;
• TauCeti.exists_eLpNorm_edist_le — the quantizer itself: some measurable map with finitely many values has a displacement of arbitrarily small L^p (μ) seminorm;
• TauCeti.exists_map_wassersteinEDist_le — the approximation theorem in quantizer form: some measurable map with finitely many values pushes μ to within ε of itself;
• TauCeti.exists_ae_mem_finset_wassersteinEDist_le — its measure form, with the approximating law carried by a finite set and again of finite p-moment, assuming measurable singletons;
• TauCeti.WassersteinSpace.dense_setOfPred_ae_mem_finset — the finitely supported laws are dense in P_p (X) on a pseudometric ground space with [StandardBorelSpace X], [BorelSpace X], and [SecondCountableTopology X];
• TauCeti.exists_natWeights_wassersteinEDist_le — all three steps combined: a law of finite moment is within 3 * δ of a law with natural multiplicities on finitely many terms of a dense sequence.
• TauCeti.wassersteinQuantizationError and TauCeti.tendsto_wassersteinQuantizationError — the N-point quantization error and its convergence to 0.

Implementation notes

TauCeti.wassersteinQuantizationError is an infimum over competitors, so it is defined without any hypothesis on the ground space and carries no attainment claim: a best N-point quantizer need not exist at this generality, and the rate at which the error decays is a separate question with its own hypotheses. Only TauCeti.tendsto_wassersteinQuantizationError uses the approximation theorem.

TauCeti.exists_map_range_wassersteinEDist_le takes the measurability of the ground distance explicitly, so that a caller with a Borel structure can supply it and one without can still use the estimate.

The approximation theorem is stated with a target accuracy ε : ℝ≥0∞ rather than as a limit along a sequence of quantizers, because the sequence of cutoffs is chosen after the radius and the two are not indexed by a single parameter.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 6, where the density of finitely supported laws in P_p (X) is used to reduce statements about general laws to finite ones.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §5.1.
• S. Graf and H. Luschgy, Foundations of Quantization for Probability Distributions, Lecture Notes in Mathematics 1730, Springer 2000, Chapter I, for the quantization error.

theorem TauCeti.wassersteinEDist_sum_smul_dirac_le {X : Type u} [MeasurableSpace X] [PseudoEMetricSpace X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (p : ENNReal) {s : Finset X} {x₀ : X} {a b : X → ENNReal} (hab : ∀ y ∈ s, y ≠ x₀ → b y ≤ a y) (hfin : ∀ y ∈ s, y ≠ x₀ → a y ≠ ⊤) (hsum : ∑ x ∈ s, b x = ∑ x ∈ s, a x) : wassersteinEDist p (∑ x ∈ s, a x • MeasureTheory.Measure.dirac x) (∑ x ∈ s, b x • MeasureTheory.Measure.dirac x) ≤ MeasureTheory.eLpNorm (fun (x : X) => edist x x₀) p (∑ y ∈ s, (a y - b y) • MeasureTheory.Measure.dirac y)

Perturbing the weights of a finitely supported law. If the weights b are below the weights a away from a distinguished point x₀ (which need not lie in the carrier s) and the two total masses agree, then all the excess mass travels to x₀, so the transport cost is at most the L^p seminorm of the distance to x₀ against the excess measure.

theorem TauCeti.exists_nat_weights_wassersteinEDist_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [MeasurableSingletonClass X] (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hp0 : p ≠ 0) (hp : p ≠ ⊤) {ν : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure ν] {s : Finset X} (hν : ν (↑s)ᶜ = 0) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (m : X → ℕ), 0 < ∑ x ∈ s, m x ∧ wassersteinEDist p ν ((∑ x ∈ s, ↑(m x))⁻¹ • ∑ x ∈ s, ↑(m x) • MeasureTheory.Measure.dirac x) ≤ ε

Rounding the weights to a common denominator. A probability measure carried by a finite set is approximated, in p-Wasserstein distance and for a finite exponent p ≠ 0, by measures whose weights are the multiples of a common unit: those of the shape (∑ m)⁻¹ • ∑ m x • δ_x for natural multiplicities m.

theorem TauCeti.exists_map_range_wassersteinEDist_le {X : Type u} [MeasurableSpace X] [PseudoMetricSpace X] {u : ℕ → X} (hd : Measurable fun (z : X × X) => edist z.1 z.2) (hu : DenseRange u) {δ : ℝ} (hδ : 0 < δ) (ν : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure ν] (p : ENNReal) : ∃ (T : X → X), Measurable T ∧ (∀ (x : X), T x ∈ Set.range u) ∧ wassersteinEDist p ν (MeasureTheory.Measure.map T ν) ≤ ENNReal.ofReal δ

Quantizing to a dense sequence. A probability measure is within any prescribed accuracy of its pushforward along a measurable map taking values in the range of a dense sequence: sending a point to the first term of the sequence closer to it than the accuracy is such a map.

theorem TauCeti.exists_eLpNorm_edist_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] {μ : MeasureTheory.Measure X} {ε : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) [MeasureTheory.IsProbabilityMeasure μ] (hμ : HasFiniteMoment p μ) (hε : ε ≠ 0) : ∃ (s : Finset X) (T : X → X), Measurable T ∧ (∀ (x : X), T x ∈ s) ∧ MeasureTheory.eLpNorm (fun (x : X) => edist x (T x)) p μ ≤ ε

A quantizer with small displacement. On a separable ground space, for a probability measure with finite p-moment and a finite exponent 1 ≤ p < ∞, some measurable map taking finitely many values moves points by a displacement x ↦ edist x (T x) of arbitrarily small L^p (μ) seminorm.

theorem TauCeti.exists_map_wassersteinEDist_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] {μ : MeasureTheory.Measure X} {ε : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) [MeasureTheory.IsProbabilityMeasure μ] (hμ : HasFiniteMoment p μ) (hε : ε ≠ 0) : ∃ (s : Finset X) (T : X → X), Measurable T ∧ (∀ (x : X), T x ∈ s) ∧ wassersteinEDist p μ (MeasureTheory.Measure.map T μ) ≤ ε

Approximation by a quantizer. On a separable ground space, a probability measure with finite p-moment and a finite exponent 1 ≤ p < ∞ is pushed to within any prescribed accuracy of itself by a measurable map taking finitely many values.

theorem TauCeti.exists_ae_mem_finset_wassersteinEDist_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] {μ : MeasureTheory.Measure X} {ε : ENNReal} [MeasurableSingletonClass X] (hp : 1 ≤ p) (hp_top : p ≠ ⊤) [MeasureTheory.IsProbabilityMeasure μ] (hμ : HasFiniteMoment p μ) (hε : ε ≠ 0) : ∃ (s : Finset X) (ν : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure ν ∧ ν (↑s)ᶜ = 0 ∧ HasFiniteMoment p ν ∧ wassersteinEDist p μ ν ≤ ε

Approximation by a finitely supported law. On a separable ground space with measurable singletons, a probability measure with finite p-moment and a finite exponent 1 ≤ p < ∞ is within any prescribed accuracy of a probability measure carried by a finite set, which again has finite p-moment.

theorem TauCeti.WassersteinSpace.dense_setOfPred_ae_mem_finset {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] [SecondCountableTopology X] [Fact (1 ≤ p)] (hp_top : p ≠ ⊤) : Dense {μ : WassersteinSpace p X | ∃ (s : Finset X), ↑↑μ (↑s)ᶜ = 0}

The finitely supported laws are dense in P_p (X). On a pseudometric ground space with [StandardBorelSpace X], a compatible [BorelSpace X], and [SecondCountableTopology X], and for a finite exponent 1 ≤ p < ∞, every finite-moment law is a Wasserstein limit of laws carried by finite sets.

theorem TauCeti.exists_natWeights_wassersteinEDist_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [StandardBorelSpace X] [BorelSpace X] {u : ℕ → X} (hu : DenseRange u) (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hμ : HasFiniteMoment p μ) {δ : ℝ} (hδ : 0 < δ) : ∃ (S : Finset X) (m : X → ℕ), (∀ x ∈ S, x ∈ Set.range u) ∧ 0 < ∑ x ∈ S, m x ∧ wassersteinEDist p μ ((∑ x ∈ S, ↑(m x))⁻¹ • ∑ x ∈ S, ↑(m x) • MeasureTheory.Measure.dirac x) ≤ ENNReal.ofReal (3 * δ)

Approximation by laws with rational weights on a dense sequence: a law of finite p-moment is within 3 * δ in W_p of a law with natural multiplicities on finitely many terms of the dense sequence u, by the three imported approximation steps (finite support, moving the atoms onto terms of u, rounding the weights) each costing δ.

noncomputable def TauCeti.wassersteinQuantizationError {X : Type u} [MeasurableSpace X] [EDist X] (p : ENNReal) (N : ℕ) (μ : MeasureTheory.Measure X) : ENNReal

The N-point quantization error of μ at exponent p: the infimum of the Wasserstein distances from μ to the probability measures carried by a set of at most N points.

This is an infimum, not a minimum: a best N-point quantizer need not exist at this generality.

theorem TauCeti.wassersteinQuantizationError_le {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {μ ν : MeasureTheory.Measure X} {N : ℕ} (hν : MeasureTheory.IsProbabilityMeasure ν) (hs : ∃ (s : Finset X), s.card ≤ N ∧ ν (↑s)ᶜ = 0) : wassersteinQuantizationError p N μ ≤ wassersteinEDist p μ ν

Every competitor bounds the quantization error from above.

theorem TauCeti.le_wassersteinQuantizationError {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {μ : MeasureTheory.Measure X} {N : ℕ} {a : ENNReal} (h : ∀ (ν : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure ν → (∃ (s : Finset X), s.card ≤ N ∧ ν (↑s)ᶜ = 0) → a ≤ wassersteinEDist p μ ν) : a ≤ wassersteinQuantizationError p N μ

A bound valid for every admissible competitor bounds the quantization error from below.

theorem TauCeti.wassersteinQuantizationError_lt_iff {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {μ : MeasureTheory.Measure X} {N : ℕ} {a : ENNReal} : wassersteinQuantizationError p N μ < a ↔ ∃ (ν : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure ν ∧ (∃ (s : Finset X), s.card ≤ N ∧ ν (↑s)ᶜ = 0) ∧ wassersteinEDist p μ ν < a

The quantization error is below a strict threshold exactly when an admissible competitor is below that threshold.

theorem TauCeti.wassersteinQuantizationError_antitone {X : Type u} [MeasurableSpace X] {p : ENNReal} [EDist X] {μ : MeasureTheory.Measure X} : Antitone fun (N : ℕ) => wassersteinQuantizationError p N μ

The quantization error decreases as more points are allowed.

theorem TauCeti.tendsto_wassersteinQuantizationError {X : Type u} [MeasurableSpace X] {p : ENNReal} [PseudoMetricSpace X] [OpensMeasurableSpace X] [TopologicalSpace.SeparableSpace X] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) [MeasureTheory.IsProbabilityMeasure μ] (hμ : HasFiniteMoment p μ) : Filter.Tendsto (fun (N : ℕ) => wassersteinQuantizationError p N μ) Filter.atTop (nhds 0)

The quantization error vanishes. On a separable ground space with measurable singletons and for a finite exponent 1 ≤ p < ∞, the N-point quantization error of a law with finite p-moment tends to 0. No rate is claimed: a quantitative bound needs further hypotheses on the law.