Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.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…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…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…The Bounded Lipschitz Vector Fields are Dense in the Square-Integrable Vector Fields Against a Probability Measure
lemmalem:lipschitz-fields-dense-l2-euclidean-2026aAnalysisProbabilityEvery square-integrable vector field against a probability measure on Euclidean space is approximated in mean square, to any accuracy, by a bounded Lipschitz vector field.Inner and Outer Regularity of a Finite Borel Measure on a Metric Space, and Lipschitz Approximation of Indicators
lemmalem:regularity-finite-borel-measure-metric-2026aAnalysisProbabilityEvery Borel set is squeezed between a closed set and an open set of nearly the same finite Borel measure, so the measure is the supremum of the measures of the closed subsets and the infimum of those of the open supersets; consequently the indicator of a Borel set is approximated…The Optimal Maps of a Uniquely Mapped Pair and of Its Reverse are Mutually Inverse Almost Everywhere
lemmalem:optimal-map-inverse-euclidean-2026aAnalysisProbabilityIf a pair and its reverse are both uniquely mapped, the two optimal maps compose to the identity almost everywhere with respect to each measure.Optimal Transport Maps and Uniquely Mapped Pairs of Probability Measures
definitiondef:optimal-transport-map-euclidean-2026aAnalysisProbabilityAn optimal map transports the first measure to the second and induces an optimal coupling; a pair is uniquely mapped when its optimal coupling is unique and induced by such a map.Brenier's Theorem: Optimal Couplings out of an Absolutely Continuous Measure are Induced by a Unique Map
theoremthm:brenier-optimal-map-euclidean-2026aAnalysisProbabilityWhen the first measure is absolutely continuous, every optimal coupling is induced by a Borel map which is the gradient of a convex function almost everywhere; the optimal coupling and the map are unique.A Coupling Concentrated on the Graph of a Borel Map is the Push-Forward by That Map
lemmalem:coupling-graph-pushforward-euclidean-2026aAnalysisProbabilityIf a coupling gives full measure to the graph of a Borel map, then it is the push-forward of its first marginal by that map, and the map transports the first marginal to the second.The Support of an Optimal Coupling is Cyclically Monotone
lemmalem:optimal-coupling-cyclically-monotone-euclidean-2026aAnalysisProbabilityThe support of an optimal coupling of two probability measures with finite second moment is a cyclically monotone set.Absolutely Continuous Probability Measure on Euclidean Space
definitiondef:absolutely-continuous-probability-measure-euclidean-2026aAnalysisProbabilityA probability measure on Euclidean space is absolutely continuous when it gives measure zero to every Borel set of Lebesgue measure zero.