Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.Atomless Probability Measure on Euclidean Space
definitiondef:atomless-measure-euclidean-2026aAnalysisProbabilityA probability measure on Euclidean space is atomless if every one-point set is null for it.Out of an Absolutely Continuous Measure the Optimal Map and the Optimal Displacement are Tangent
corollarycor:optimal-displacement-tangent-wasserstein-2026aAnalysisProbabilityWhen the source measure is absolutely continuous the pair is uniquely mapped, and both the optimal map and the identity minus the optimal map belong to the tangent space of the Wasserstein space at the source.A Square-Integrable Selection of the Subdifferential of a Convex Potential Belongs to the Tangent Space
theoremthm:convex-potential-gradient-tangent-wasserstein-2026aAnalysisProbabilityIf a Borel vector field is, almost everywhere with respect to a measure with finite second moment, the unique subgradient of a convex function on an open convex set of full measure, and is square-integrable, then it belongs to the tangent space of the Wasserstein space at that me…Mollification of a Lipschitz Convex Function: Smooth Convex Approximations with Bounded Gradients Converging Where the Subgradient is Unique
lemmalem:mollified-convex-gradient-convergence-rn-2026aAnalysisThe mollifications of a convex function that is Lipschitz with a given constant are smooth, convex and Lipschitz with the same constant, with gradients bounded by it; at a point where the subdifferential is a single vector the gradients of the mollifications converge to that vect…The Lipschitz Truncation of a Convex Function: a Global Lipschitz Convex Minorant Agreeing with It Where the Slope is Small
lemmalem:lipschitz-truncation-convex-rn-2026aAnalysisInfimal convolution of a convex function on an open convex set with a multiple of the norm produces a convex function on the whole space, Lipschitz with that multiple as constant, lying below the original; at a point whose subgradients are bounded by the constant the two function…Mean-Square Stability of the Optimal Map on the Space of Square-Integrable Random Vectors
lemmalem:optimal-map-stability-lift-wasserstein-2026aAnalysisProbabilityFor a uniquely mapped pair, composing a random vector of the first law with the optimal map gives a square-integrable random vector of the second law, and along any pair of sequences of the two laws whose mean-square distances tend to the Wasserstein distance the composition appr…Mean-Square Stability of the Optimal Map of a Uniquely Mapped Pair Along Couplings of Nearly Optimal Cost
theoremthm:optimal-map-stability-euclidean-2026aAnalysisProbabilityIf a pair of measures with finite second moment is uniquely mapped, then along any sequence of couplings whose quadratic costs tend to the squared Wasserstein distance the mean-square discrepancy between the second coordinate and the image of the first under the optimal map tends…A Function Nondecreasing on a Borel Subset of the Real Line and Vanishing Outside It is Borel
lemmalem:monotone-borel-subset-real-2026aAnalysisIf a real function is nondecreasing on a Borel subset of the real line and vanishes off that subset, then it is Borel measurable.A Closed Subset of a Euclidean Space is a Countable Union of Compact Sets, and Its Coordinate Projections are Borel
lemmalem:projection-closed-set-borel-euclidean-2026aAnalysisA closed subset of a Euclidean space is exhausted by its intersections with the closed balls about the origin, each compact; consequently the image of a closed subset of a product under either coordinate projection is a Borel set.Nonnegative Combinations of Two Finite Measures, and the Average of Two Couplings
lemmalem:average-couplings-euclidean-2026aAnalysisProbabilityA nonnegative combination of two finite measures is a finite measure whose integrals are the corresponding combination of the integrals; applied with weights one half to two couplings of the same pair of measures it produces a coupling whose quadratic cost is the average of the t…Test Functions Approximate Bounded Continuous Functions Pointwise, Determine a Finite Borel Measure, and Detect a Vanishing Density
lemmalem:test-functions-determine-measure-euclidean-2026aAnalysisProbabilityEvery bounded continuous function on Euclidean space is a pointwise limit of test functions bounded by the same constant; consequently two finite Borel measures that integrate every test function alike are equal, and an integrable Borel function whose products with all test funct…