Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.The Metric Subspace: Continuity, the Borel Sigma-Algebra, and the Restriction of a Borel Measure
lemmalem:borel-subspace-metric-2026aAnalysisTopologyThe Borel sets of a metric subspace are the traces of the ambient Borel sets; when the subspace is itself Borel they are the ambient Borel sets it contains, the restriction of a Borel measure is a Borel measure on it, and an integral of a function vanishing off the subspace is co…Compact Subsets of a Metric Space are Closed and Borel
lemmalem:compact-subset-closed-borel-metric-2026aAnalysisTopologyA compact subset of a metric space is closed, and therefore belongs to the Borel sigma-algebra, as does its complement.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…Existence, Penalty Bounds and Optimal Realisation at a Maximiser of the Wasserstein-Doubled Difference on the Lift
lemmalem:doubling-maximiser-lift-wasserstein-2026bAnalysisPDEFor a Wasserstein-coercive pair the Wasserstein-doubled difference of the delta-envelopes attains its supremum, the penalty and second moment are bounded at a near-maximiser independently of the doubling strength, the penalised distance vanishes along a doubling sequence, and the…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.Viscosity Subsolution, Supersolution and Solution on the Lift of the Wasserstein Space
definitiondef:viscosity-lift-wasserstein-2026bAnalysisPDEA bounded-near-each-point function on the Wasserstein space is a viscosity subsolution (supersolution) on the lift if, wherever its delta-envelope composed with the law map minus a lifted test function has a local maximum (minimum) on the lift of the penalty domain, the shifted o…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…The Shift-Semicontinuity Condition for an Equation Operator on the Lift of the Wasserstein Space
definitiondef:shift-semicontinuity-condition-lift-wasserstein-2026aAnalysisProbabilityPDESays that the lower shift of the operator passes to the limit from below, and the upper shift from above, along sequences of test data with bounded score whose lifted scores converge weakly.The Shift-Coercivity Condition for an Equation Operator on the Lift of the Wasserstein Space
definitiondef:shift-coercivity-condition-lift-wasserstein-2026aAnalysisProbabilityPDESays that on the test data admitted at a level, the shifts of the operator force the score of the penalty pair to be bounded.Locally Strictly Proper Second-Order Equation Operator on the Lift of the Wasserstein Space
definitiondef:locally-strictly-proper-lift-wasserstein-2026aAnalysisProbabilityPDESays that the operator increases in its value argument at a strictly positive rate, uniform over each bounded range of values.Test Data for a Second-Order Equation Operator on the Lift of the Wasserstein Space and the Admissible Sets
definitiondef:test-data-lift-wasserstein-2026aAnalysisProbabilityPDEFixes the quadruples of arguments that a second-order equation operator on the lift and its shifts accept, what it means for such a datum to be bounded at a level, and the two sets of data admitted at a level.Existence and Basic Estimates at a Maximiser of the Gauge-Doubled Difference on the Wasserstein Space
lemmalem:doubling-maximiser-wasserstein-2026aAnalysisProbabilityPDEFor a coercive penalty pair the difference of the delta-envelopes penalised by the squared centred heat gauge attains its supremum; at any maximiser the penalty and the second moment are bounded independently of the doubling strength, and if the two functions are Lipschitz for th…Basic Properties of a Coercive Penalty Pair: a Lower Bound for the Penalty, Semicontinuity, and Exact Delta-Envelopes
lemmalem:coercive-penalty-pair-basic-wasserstein-2026aAnalysisProbabilityThe penalty of a coercive penalty pair is bounded below on its domain and lower semicontinuous both for the centred heat gauge and for the Wasserstein distance, so that the delta-envelopes of a continuous function are exactly the shifted function.