Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.Cyclically Monotone Subset of a Doubled Euclidean Space
definitiondef:cyclically-monotone-set-euclidean-2026aAnalysisA subset of a doubled Euclidean space is cyclically monotone when every finite cycle of its points has nonpositive chain sum.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.The Support of a Borel Measure is Closed, and Carries Full Measure on a Separable Space
lemmalem:support-closed-full-measure-metric-2026aAnalysisThe support of a Borel measure on a metric space is closed, and on a separable space its complement is null.- Euclidean space with its usual distance has a countable dense subset.
Support of a Borel Measure on a Metric Space
definitiondef:support-borel-measure-metric-2026aAnalysisThe support of a Borel measure on a metric space is the set of points all of whose open balls have positive measure.A Comparison Principle for Viscosity Solutions on the Lift of the Wasserstein Space
theoremthm:comparison-lift-wasserstein-2026aAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair with closed score and an operator that is locally strictly proper and satisfies the shift-coercivity, shift-semicontinuity and second-order structure conditions, a bounded viscosity subsolution on the lift lies below a bounded viscosity sup…The Structure Estimate at a Maximiser of the Wasserstein-Doubled Difference on the Lift
lemmalem:comparison-estimate-lift-wasserstein-2026aAnalysisProbabilityPDEAt a maximiser of the Wasserstein-doubled difference of the delta-envelopes, the optimally coupled lift lies in the score domain, and the maximal value is bounded by the two moduli of a second-order structure pair evaluated at the penalised distance and at the scaled penalty.The Doubled Difference on the Lift of a Wasserstein-Coercive Penalty Pair: Bounds, Closed Superlevel Sets and the Least Penalty
lemmalem:doubled-difference-lift-wasserstein-2026aAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair, the penalty attains a least value, and the lifts of the delta-envelopes of a bounded upper semicontinuous function and a bounded lower semicontinuous function are bounded and have closed superlevel sets, as does the quadratically doubled d…Lifted Test Data from Second-Order Data on the Space of Square-Integrable Random Vectors: Compression along the Constant Tuple
lemmalem:compression-lifted-test-data-wasserstein-2026aAnalysisProbabilityPDEEvery function of class on the lift is a lifted test function whose translation Hessian is the compression of its Hilbert Hessian along the constant tuple; quadruples approximable by test data therefore produce lifted test functions with compressed matrices, and the second-…Compression of a Bounded Symmetric Bilinear Form along an Orthonormal Tuple
lemmalem:form-compression-hilbert-2026aAnalysisLinear AlgebraThe matrix of values of a bounded symmetric bilinear form on an orthonormal tuple is symmetric and its quadratic form is that of the original form along the span of the tuple; the compression is linear, does not increase the norm, preserves the order, sends the tail form to zero,…The Constant Tuple on : Coordinates, Projection, Tail Form, and Translation-Closed Preimages
lemmalem:constants-tuple-lift-wasserstein-2026aAnalysisProbabilityThe constant classes at the standard basis vectors form an orthonormal tuple in the space of square-integrable random vectors whose coordinate map is the mean of the law, whose projection is the constant class at that mean, and whose tail form is the centred second moment; preima…