Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Penalty-Subordinate Growth of a Function on the Penalty Domain
definitiondef:penalty-subordinate-growth-wasserstein-2026aAnalysisProbabilityA function on the penalty domain has penalty-subordinate growth from above if, for every positive delta, it is bounded above by a constant plus delta times the penalty; growth from below is the mirror condition.Perron's Method on the Wasserstein Space: Existence of a Viscosity Solution Between a Subsolution and a Supersolution
theoremthm:perron-existence-wasserstein-2026cAnalysisProbabilityPDEFor a Wasserstein-closed penalty pair with regular penalised maxima whose penalty domain has the map property, and a degenerate elliptic operator, the pointwise supremum of all viscosity subsolutions on the penalty domain lying between a given subsolution and a given supersolutio…The Bump Construction on the Wasserstein Space: the Local Maximum of a Viscosity Subsolution and a Penalised Intrinsic Test Function
lemmalem:perron-bump-wasserstein-2026cAnalysisProbabilityPDEInside a Wasserstein ball, replace a viscosity subsolution v on the penalty domain by the maximum of v and an intrinsic test function, bounded above on the ball, minus a multiple of the penalty, which stays below v near the edge of the ball. If the test function satisfies the shi…The Pointwise Supremum of a Uniformly Subordinate Family of Viscosity Subsolutions on the Wasserstein Space is a Viscosity Subsolution
lemmalem:sup-of-subsolutions-wasserstein-2026cAnalysisProbabilityPDEFor a Wasserstein-closed penalty pair whose penalty domain has the map property, the pointwise supremum of a nonempty family of viscosity subsolutions on the penalty domain that is uniformly subordinate from above (for each positive delta, one constant plus delta times the penalt…Attained Maxima on Closed Balls of the Penalty Domain, for a Wasserstein-Coercive Penalty Pair
lemmalem:penalised-usc-attains-ball-wasserstein-2026bAnalysisProbabilityFor a Wasserstein-coercive penalty pair, an upper semicontinuous function on the penalty domain that lies below a constant minus a positive multiple of the penalty on a closed ball attains its supremum on that ball.Penalty Pairs with Regular Penalised Maxima
definitiondef:regular-penalised-maxima-wasserstein-2026bAnalysisProbabilityPDEA penalty pair has regular penalised maxima when every local maximiser, on the penalty domain, of an intrinsic test function minus a positive multiple of the penalty lies in the score domain.The Structure Estimate at a Maximiser of the Wasserstein-Doubled Difference
lemmalem:comparison-estimate-wasserstein-2026dAnalysisPDEFor a bounded-above viscosity subsolution and a bounded-below viscosity supersolution on the penalty domain, a nonnegative supremum of the Wasserstein-doubled difference of their delta-envelopes is attained at a pair in the score domain at which the properness constant times the…Intrinsic Test Functions at a Maximiser of the Wasserstein-Doubled Difference
lemmalem:doubling-test-functions-wasserstein-2026cAnalysisPDEAt a maximiser of the Wasserstein-doubled difference of the delta-envelopes of two bounded functions over a penalty domain with the map property, there is a maximising pair and a pair of matrices admitted by Ishii's lemma such that each side is touched, arbitrarily close by, by i…A Triangle Inequality for Discrepancies Along a Composite Coupling
lemmalem:discrepancy-gluing-wasserstein-2026aAnalysisProbabilityAlong the composite of two couplings obtained by gluing, the square root of the discrepancy between a field on the first measure and a field on the third is at most the sum of the square roots of the discrepancies through any field on the middle measure.The Displacement Midpoint and the Midpoint Split of the Squared Wasserstein Distance
lemmalem:midpoint-split-wasserstein-2026aAnalysisProbabilityThe midpoint of an optimal coupling of two measures lies at a quarter of their squared distance from each, and the squared Wasserstein distance between any two measures is bounded by twice the centred squared distances of each to that midpoint plus the squared distance of their m…A Comparison Principle for Viscosity Solutions on the Wasserstein Space
theoremthm:comparison-wasserstein-2026dAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair with closed score along couplings whose penalty domain has the map property, and an operator that is locally strictly proper and satisfies the shift-coercivity, shift-semicontinuity and second-order structure conditions: if u is a viscosity…Existence, Penalty Bounds and Monotonicity of the Maximum of the Wasserstein-Doubled Difference of Bounded Functions
lemmalem:w2-doubling-maximiser-wasserstein-2026bAnalysisPDEFor a Wasserstein-coercive penalty pair and functions bounded above and below on the penalty domain, the Wasserstein-doubled difference of their delta-envelopes attains its supremum; the penalty is bounded by a constant over delta wherever that difference is nonnegative; and the…The Second-Order Structure Condition at Uniquely Mapped Pairs on the Wasserstein Space
definitiondef:second-order-structure-condition-wasserstein-2026bAnalysisPDEThe intrinsic twin of the structure condition on the lift: at pairs of measures uniquely mapped in both directions, with the doubling momenta given by the optimal displacements and a pair of matrices admitted by Ishii's lemma, the difference of the shifted operators is bounded be…The Shift-Semicontinuity Condition for an Equation Operator on the Wasserstein Space
definitiondef:shift-semicontinuity-condition-wasserstein-2026cAnalysisPDEAn intrinsic equation operator is shift-semicontinuous if its lower shift is lower semicontinuous and its upper shift upper semicontinuous along bounded test data converging along couplings of vanishing cost, the fields strongly and the scores weakly.The Shift-Coercivity Condition for an Equation Operator on the Wasserstein Space
definitiondef:shift-coercivity-condition-wasserstein-2026bAnalysisPDEAn intrinsic equation operator satisfies the shift-coercivity condition if, for every shift size and every level, the scores of the measures carrying admissible test data are uniformly bounded.Locally Strictly Proper Second-Order Equation Operator on the Wasserstein Space
definitiondef:locally-strictly-proper-wasserstein-2026aAnalysisPDEAn intrinsic equation operator on the Wasserstein space is locally strictly proper if on every bounded range of the value argument it increases in that argument at least linearly with a positive rate, uniformly in the measure, the field and the matrix.Penalty Pairs with Closed Score Along Couplings
definitiondef:closed-score-along-couplings-wasserstein-2026bAnalysisProbabilityA penalty pair has closed score along couplings if, whenever measures of the score domain with uniformly bounded scores approach a measure of the penalty domain along couplings of vanishing cost, the limit lies in the score domain and the scores converge weakly along those coupli…Strong and Weak Convergence of Vector Fields Along Couplings of Vanishing Cost
definitiondef:field-convergence-along-couplings-wasserstein-2026aAnalysisProbabilityVector fields against a sequence of measures converge to a field against a limit measure along couplings whose cost tends to zero: strongly when their discrepancy along the couplings tends to zero, weakly when their cross pairing with every fixed field against the limit tends to…The Cross Pairing of Two Square-Integrable Vector Fields Along a Coupling
lemmalem:coupling-cross-pairing-wasserstein-2026aAnalysisProbabilityFor a coupling of two measures and square-integrable vector fields against each, the integral of the dot product of the first field at the first coordinate with the second field at the second coordinate is well defined, bounded by the product of the norms, bilinear, related to th…The Squared Wasserstein Distance to a Fixed Measure and Functions of the Mean are Intrinsic Test Functions
lemmalem:w2-squared-intrinsic-test-function-wasserstein-2026bAnalysisProbabilityOn a set of measures with the map property, the squared Wasserstein distance to a fixed measure is an intrinsic test function whose gradient is twice the optimal displacement and whose translation Hessian is twice the identity; a twice continuously differentiable function of the…