Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Triangle Inequality for Discrepancies Along a Composite Coupling
lemmalem:discrepancy-gluing-wasserstein-2026aAnalysisProbabilityAlong the composite of two couplings obtained by gluing, the square root of the discrepancy between a field on the first measure and a field on the third is at most the sum of the square roots of the discrepancies through any field on the middle measure.The Displacement Midpoint and the Midpoint Split of the Squared Wasserstein Distance
lemmalem:midpoint-split-wasserstein-2026aAnalysisProbabilityThe midpoint of an optimal coupling of two measures lies at a quarter of their squared distance from each, and the squared Wasserstein distance between any two measures is bounded by twice the centred squared distances of each to that midpoint plus the squared distance of their m…A Comparison Principle for Viscosity Solutions on the Wasserstein Space
theoremthm:comparison-wasserstein-2026dAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair with closed score along couplings whose penalty domain has the map property, and an operator that is locally strictly proper and satisfies the shift-coercivity, shift-semicontinuity and second-order structure conditions: if u is a viscosity…Penalty Pairs with Closed Score Along Couplings
definitiondef:closed-score-along-couplings-wasserstein-2026bAnalysisProbabilityA penalty pair has closed score along couplings if, whenever measures of the score domain with uniformly bounded scores approach a measure of the penalty domain along couplings of vanishing cost, the limit lies in the score domain and the scores converge weakly along those coupli…Strong and Weak Convergence of Vector Fields Along Couplings of Vanishing Cost
definitiondef:field-convergence-along-couplings-wasserstein-2026aAnalysisProbabilityVector fields against a sequence of measures converge to a field against a limit measure along couplings whose cost tends to zero: strongly when their discrepancy along the couplings tends to zero, weakly when their cross pairing with every fixed field against the limit tends to…The Cross Pairing of Two Square-Integrable Vector Fields Along a Coupling
lemmalem:coupling-cross-pairing-wasserstein-2026aAnalysisProbabilityFor a coupling of two measures and square-integrable vector fields against each, the integral of the dot product of the first field at the first coordinate with the second field at the second coordinate is well defined, bounded by the product of the norms, bilinear, related to th…The Squared Wasserstein Distance to a Fixed Measure and Functions of the Mean are Intrinsic Test Functions
lemmalem:w2-squared-intrinsic-test-function-wasserstein-2026bAnalysisProbabilityOn a set of measures with the map property, the squared Wasserstein distance to a fixed measure is an intrinsic test function whose gradient is twice the optimal displacement and whose translation Hessian is twice the identity; a twice continuously differentiable function of the…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.