How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The Euclidean quadratic Wasserstein space
Definition
For an integer , let have its Euclidean norm and Borel sigma-algebra. Define to be the Borel probability measures with . A coupling of is a Borel probability measure on whose first and second coordinate marginals are and ; write for the set of couplings. Define
Definition references
def borel probability law on a polish space
def expectation of a nonnegative or integrable random variable
def product sigma algebra and finite product sigma algebras
lem borel product of second countable spaces
Filippo Santambrogio, Optimal Transport for Applied Mathematicians, Chapter 5, §§5.1–5.3
Facts & Assumptions
Given: An integer and .
The product of two probability measures exists, is a probability, and has the two given marginals. The product measure of two sigma-finite measure spaces For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
For a nonnegative function on a product probability space, Tonelli identifies its integral with either iterated integral; . Tonelli's theorem for nonnegative measurable functions on a sigma-finite product Expectation of a nonnegative or integrable random variable
Proof
The product law is a Borel probability on with marginals by [F1], so it belongs to . Thus the coupling set in the definition is nonempty.
By the inequality in [F2] and the finite second moments of , Tonelli gives All coupling costs are nonnegative, so their infimum is finite and nonnegative; its square root in the displayed definition is therefore a finite real number.
Depends on
- Borel probability law on a polish space
- Probability measures and probability spaces
- Expectation of a nonnegative or integrable random variable
- The product sigma-algebra and its finite iterates
- Borel sigma-algebra of a product of second-countable spaces
- Polish spaces are separable completely metrizable spaces
- The product measure of two sigma-finite measure spaces
- For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
Used by
- Absolutely continuous curves of order two in Wasserstein space Definition
- Finite-action continuity equation in Euclidean space Definition
- Generalized W2 geodesics and strong Wasserstein subgradients Definition
- Wasserstein gradient flow for a feature-measure energy Definition
- An isotropic Gaussian Wasserstein geodesic Example
- Exact quadratic feature-energy flow and particle limit Example
- The Gaussian coupling bound is exact for a point mass Example
- Translation of a Dirac mass Example
- Derivative of squared W2 distance along a finite-action continuity equation Lemma
- Feature energy is W2-continuous on a common cutoff Lemma
- Gluing two Euclidean couplings Lemma
- One-sided semiconvex characteristics give W2 uniqueness and stability Lemma
- Partial one-homogeneous energy is continuous under W2 convergence Lemma
- The Hilbert lift induces the localized Wasserstein continuity equation Lemma
- The selected pointwise field is a strong Wasserstein subgradient Lemma
- W2 convergence implies weak convergence of homogeneous projections Lemma
- Optimal quadratic couplings exist and their cost is weakly lower semicontinuous Proposition
- AC2 curves admit a unique minimum-action velocity field Theorem
- Finite-action continuity equations generate AC2 Wasserstein curves Theorem
- Finite-particle flows converge to the measure-valued flow in W2 Theorem
- Gaussian smoothing converges weakly at the endpoint Theorem
- Metric derivatives of AC2 Wasserstein curves Theorem
- Particle number and training time limits interchange qualitatively Theorem
- The quadratic Wasserstein distance is a metric Theorem
- The quadratic Wasserstein space is complete Theorem
- The topology of W2 is narrow convergence plus uniform second-moment tails Theorem
Dependency tree · two levels
34 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Filippo Santambrogio, Optimal Transport for Applied Mathematicians, Chapter 5, §§5.1–5.3 (standard reference, not scraped)
- Lénaïc Chizat and Francis Bach, On the Global Convergence of Gradient Descent for Over-parameterized Models using Optimal Transport, Appendix A.1, PDF pp. 12–13 (standard reference, not scraped)