Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…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 Interior of a Convex Set is Convex and Carries Each of Its Borel Subsets up to a Null Set
lemmalem:convex-set-density-interior-rn-2026aAnalysisThe interior of a convex subset of Euclidean space is convex, and every Borel subset of the convex set lies in that interior up to a Lebesgue null set.Rockafellar's Theorem: a Cyclically Monotone Set Lies in the Subdifferential of a Convex Function
theoremthm:rockafellar-cyclically-monotone-euclidean-2026aAnalysisEvery nonempty cyclically monotone set is contained in the graph of the subdifferential of a convex function defined on a convex set containing its first projection.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.