Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Stability of the Optimal Displacement Under Perturbation of the Source Along Couplings of Vanishing Cost
lemmalem:optimal-displacement-source-stability-wasserstein-2026aAnalysisProbabilityIf a source measure is uniquely mapped to a fixed target, then optimal maps from nearby sources to the same target, compared along couplings of vanishing cost, converge in mean square to its optimal map, and so do the optimal displacements.First- and Second-Order Conditions at a Penalised Extremum of an Intrinsic Test Function on the Wasserstein Space
lemmalem:penalised-extremum-intrinsic-wasserstein-2026cAnalysisProbabilityAt a point of the score domain at which an intrinsic test function minus a positive multiple of the penalty has a local maximum on the penalty domain, the gradient along couplings equals that multiple of the score and the translation Hessian is at most that multiple of the transl…Restrictions, Sums, Real Multiples and Differences of Intrinsic Test Functions on the Wasserstein Space
lemmalem:intrinsic-test-function-linear-wasserstein-2026bAnalysisProbabilityAn intrinsic test function on a set of measures is one on every subset, and linear combinations and differences of intrinsic test functions on a set are again intrinsic test functions there, with gradients along couplings and translation Hessians depending linearly on the functio…Test Data for an Intrinsic Second-Order Equation Operator on the Wasserstein Space and the Admissible Sets
definitiondef:test-data-wasserstein-2026bAnalysisProbabilityPDEThe test data of an intrinsic second-order equation operator are a measure in the score domain, a vector field against it, a real number and a symmetric matrix; bounded test data and the admissible sets on which the structure conditions are imposed are defined from them.The Squared Wasserstein Distance to a Fixed Measure: a One-Sided Bound Along Couplings, Differentiability at a Uniquely Mapped Source, and the Translation and Centring Identities
lemmalem:w2-squared-along-couplings-wasserstein-2026aAnalysisProbabilityThe squared Wasserstein distance to a fixed measure satisfies a one-sided quadratic bound along every coupling out of a mapped source, is differentiable along couplings with gradient twice the optimal displacement when the source is uniquely mapped, and transforms explicitly unde…Intrinsic Test Functions on the Wasserstein Space and Their Translation Hessians
definitiondef:intrinsic-test-function-wasserstein-2026cAnalysisProbabilityPDEA function on the Wasserstein space is an intrinsic test function on a set of measures when it is continuous, differentiable along couplings at each point of the set with a tangent gradient, its gradient is continuous along couplings of vanishing cost within the set, and it is tw…The Intrinsic Calculus on the Wasserstein Space: Standing Notation
settingset:wasserstein-intrinsic-2026bAnalysisProbabilityPDEStanding notation for the intrinsic theory of second-order equations on the Wasserstein space: couplings and the displacement pairing, optimal maps and the map property, differentiability along couplings, and the operator and penalty vocabulary. No probability space is assumed to…Two Sufficient Conditions for the Map Property: Absolute Continuity, and Atomlessness on the Line
lemmalem:map-property-sufficient-wasserstein-2026aAnalysisProbabilityA set of absolutely continuous measures has the map property in every dimension, and on the real line a set of atomless measures has it.The Map Property of a Set of Probability Measures
definitiondef:map-property-wasserstein-2026aAnalysisProbabilityA set of measures has the map property if every pair with a source in the set is uniquely mapped and the optimal displacement out of the source is tangent.Differentiability of a Function on the Wasserstein Space Along Couplings, and Its Gradient
definitiondef:differentiable-along-couplings-wasserstein-2026aAnalysisProbabilityA function on the Wasserstein space is differentiable along couplings at a measure if its increment is the displacement pairing of a square-integrable vector field along every coupling of small cost, up to an error of smaller order; that field is the gradient.A Square-Integrable Vector Field Whose Displacement Pairings Vanish to First Order is Zero
lemmalem:coupling-derivative-unique-wasserstein-2026aAnalysisProbabilityIf the displacement pairings of a square-integrable vector field along all couplings of small cost are of smaller order than the square root of the cost, the field is zero. This is what makes a gradient along couplings unique.The Optimal Map as a Square-Integrable Vector Field: Integrability, Transport Cost and Uniqueness of the Class
lemmalem:optimal-map-class-wasserstein-2026aAnalysisProbabilityA Borel map transporting one measure to another is square-integrable against the source; for an optimal map the squared norm of its displacement is the squared Wasserstein distance; and for a uniquely mapped pair all optimal maps define the same square-integrable class.The Displacement Pairing of a Square-Integrable Vector Field Along a Coupling
lemmalem:coupling-pairing-wasserstein-2026aAnalysisProbabilityThe integral of a square-integrable vector field against the displacement of a coupling: it is well defined, bounded by the norm of the field times the square root of the cost, linear in the field, and reduces to an inner product along a displacement coupling.Gluing Two Couplings over a Common Middle Marginal, and the Composite Coupling
lemmalem:gluing-couplings-euclidean-2026aAnalysisProbabilityTwo couplings with a common middle marginal are the consecutive pairwise marginals of a single measure on the threefold product; its coordinate maps are square-integrable, and the outer pair is a coupling whose cost obeys the triangle inequality.Pairings of Borel Maps as Couplings, and Gluing Two Couplings over a Finitely Supported Middle Marginal
lemmalem:finite-middle-gluing-euclidean-2026aAnalysisProbabilityFixes the three coordinate maps of the threefold product of Euclidean space; records that the pairing of two Borel maps pushes a measure forward to a coupling of cost the mean square distance between them; and glues two couplings sharing a finitely supported middle marginal.On the Real Line the Tangent Space is the Whole Space of Square-Integrable Vector Fields
theoremthm:tangent-space-line-2026aAnalysisProbabilityFor every probability measure with finite second moment on the real line, the closure of the gradients of test functions is all of the square-integrable vector fields against it.On the Real Line an Atomless Source is Uniquely Mapped, by a Nondecreasing Optimal Map
theoremthm:monotone-optimal-map-line-2026aAnalysisProbabilityFor an atomless measure with finite second moment on the real line and any second measure with finite second moment, there is an optimal map that is nondecreasing on a Borel set of full measure, and every optimal coupling is induced by it.Test Functions on the Real Line: Unit Mass, Large Mass, Mean-Zero Correction, and the Primitive of a Mean-Zero Test Function
lemmalem:primitive-test-function-real-2026aAnalysisTest functions on the real line are Lebesgue integrable; there are nonnegative ones of unit mass, and ones bounded by one of arbitrarily large mass; subtracting a multiple of a unit-mass one makes any test function have mean zero; and a test function of mean zero is the derivativ…Cyclically Monotone Subsets of the Doubled Real Line: Two-Point Monotonicity, Ordering of the Sections, and Countability of the Multi-Valued Abscissae
lemmalem:cyclically-monotone-line-2026aAnalysisFor a cyclically monotone subset of the plane the two-point inequality holds, the section over a smaller abscissa lies below the section over a larger one, and the set of abscissae whose section has more than one point is countable.Countable Sets are Null for an Atomless Measure, One-Point Sets are Lebesgue Null, and an Absolutely Continuous Measure is Atomless
lemmalem:atomless-basic-euclidean-2026aAnalysisProbabilityAn atomless probability measure gives measure zero to every countable set; one-point sets in Euclidean space are Lebesgue null; and every absolutely continuous probability measure is atomless.