Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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-…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…Existence of an Optimal Coupling of Two Probability Measures with Finite Second Moment
theoremthm:optimal-coupling-exists-euclidean-2026aAnalysisProbabilityAny two probability measures on Euclidean space with finite second moment admit an optimal coupling: the infimum defining the quadratic Wasserstein distance is attained.The Couplings of Two Probability Measures on Euclidean Space are Closed under Weak Convergence
lemmalem:couplings-weakly-closed-euclidean-2026aAnalysisProbabilityA weak limit of couplings of two fixed probability measures on Euclidean space is again a coupling of them.Continuity of the Coordinate Projections and of the Quadratic Cost Function, and Passage of a Cost Bound to a Weak Limit
lemmalem:quadratic-cost-lsc-weak-euclidean-2026aAnalysisProbabilityThe coordinate projections of a Euclidean product are nonexpansive and the quadratic cost function is continuous; consequently a bound on the quadratic cost that holds along a weakly convergent sequence of probability measures holds in the limit.Tightness from Bounded Second Moments, and Tightness of the Couplings of Two Measures with Finite Second Moment
lemmalem:tightness-criteria-euclidean-2026aAnalysisProbabilityA family of probability measures on Euclidean space with uniformly bounded second moments is tight; the second moment of a coupling is the sum of the second moments of its marginals, so the couplings of two measures with finite second moment form a tight family.Prokhorov's Theorem on Euclidean Space: a Tight Sequence of Probability Measures Has a Weakly Convergent Subsequence
theoremthm:prokhorov-sequential-euclidean-2026aAnalysisProbabilityEvery tight sequence of Borel probability measures on a Euclidean space has a subsequence converging weakly to a Borel probability measure on that space.Tight Family of Borel Measures on a Metric Space
definitiondef:tight-family-borel-measures-metric-2026aAnalysisProbabilityA family of Borel measures on a metric space is tight when, for each tolerance, a single compact set carries all but that much of the mass of every member of the family.Optimally Coupled Pairs of Square-Integrable Random Vectors
definitiondef:optimally-coupled-pair-wasserstein-2026aAnalysisProbabilityTwo square-integrable random vectors are optimally coupled if their joint law is an optimal coupling of their laws, that is, if their mean-square distance equals the Wasserstein distance of their laws.Second-Order Equation Operators on the Lift of the Wasserstein Space and Their Delta-Shifts
definitiondef:operator-lift-wasserstein-2026aAnalysisProbabilityA second-order equation operator on the lift takes a square-integrable random vector whose law lies in a given set of measures, a real number, a second random vector, and a symmetric matrix, and depends on the two random vectors only through their joint law. Its delta-shifts rela…The Joint Law of Two Classes of Square-Integrable Random Vectors: Marginals, Cost, and Invariance Under Shifts by a Vector Field
lemmalem:joint-law-random-vectors-wasserstein-2026aAnalysisProbabilityTwo classes of square-integrable random vectors have a well-defined joint law with finite second moment, whose marginals are their laws and which is a coupling of them with cost the mean-square distance; equality of joint laws is preserved when the same vector field of the common…Penalty Pairs with Closed Score
definitiondef:closed-score-penalty-pair-wasserstein-2026bAnalysisProbabilityA penalty pair has closed score if, along any sequence of random vectors converging in mean square whose scores are uniformly bounded, the limit law lies in the score domain and the scores converge weakly to the score at the limit.Basic Properties of a Wasserstein-Coercive Penalty Pair
lemmalem:w2-coercive-penalty-pair-basic-wasserstein-2026cAnalysisProbabilityFor a Wasserstein-coercive penalty pair the second moment is bounded on each sublevel set of the penalty, and the penalty is bounded below and lower semicontinuous.Wasserstein-Coercive Penalty Pairs
definitiondef:w2-coercive-penalty-pair-wasserstein-2026cAnalysisProbabilityA penalty pair is Wasserstein-coercive if every sublevel set of its penalty is sequentially compact for the Wasserstein distance.Lifted Test Functions: Algebra, Quadratics, and the Lifts of Test Functions on the Wasserstein Space
lemmalem:lifted-test-function-basic-wasserstein-2026bAnalysisProbabilityLifted test functions are closed under sums and real multiples; affine functions and multiples of a squared distance to a point are lifted test functions, with the expected gradients and translation Hessians; and every test function on the Wasserstein space lifts to one.Lifted Test Functions on the Space of Square-Integrable Random Vectors and Their Translation Hessians
definitiondef:lifted-test-function-wasserstein-2026bAnalysisProbabilityA lifted test function is a real function on the space of square-integrable random vectors that is of class C^1 and twice continuously differentiable along translations; its translation Hessian is the Hessian at the origin of its restriction to translations.The Second-Order Structure Condition at Optimally Coupled Pairs on the Lift of the Wasserstein Space
definitiondef:second-order-structure-condition-lift-wasserstein-2026bAnalysisProbabilityPDEA pair of symmetric matrices is admitted at a doubling strength when it satisfies the ordering, norm and quadratic-form bounds of Lions' lemma; the operator satisfies the second-order structure condition when, at every level measured by the delta-scaled penalty and by the value s…