Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…Stability of the Optimal Displacement Under Perturbation of the Source Along Couplings of Vanishing Cost
lemmalem:optimal-displacement-source-stability-wasserstein-2026aAnalysisProbabilityIf a source measure is uniquely mapped to a fixed target, then optimal maps from nearby sources to the same target, compared along couplings of vanishing cost, converge in mean square to its optimal map, and so do the optimal displacements.First- and Second-Order Conditions at a Penalised Extremum of an Intrinsic Test Function on the Wasserstein Space
lemmalem:penalised-extremum-intrinsic-wasserstein-2026cAnalysisProbabilityAt a point of the score domain at which an intrinsic test function minus a positive multiple of the penalty has a local maximum on the penalty domain, the gradient along couplings equals that multiple of the score and the translation Hessian is at most that multiple of the transl…Restrictions, Sums, Real Multiples and Differences of Intrinsic Test Functions on the Wasserstein Space
lemmalem:intrinsic-test-function-linear-wasserstein-2026bAnalysisProbabilityAn intrinsic test function on a set of measures is one on every subset, and linear combinations and differences of intrinsic test functions on a set are again intrinsic test functions there, with gradients along couplings and translation Hessians depending linearly on the functio…Test Data for an Intrinsic Second-Order Equation Operator on the Wasserstein Space and the Admissible Sets
definitiondef:test-data-wasserstein-2026bAnalysisProbabilityPDEThe test data of an intrinsic second-order equation operator are a measure in the score domain, a vector field against it, a real number and a symmetric matrix; bounded test data and the admissible sets on which the structure conditions are imposed are defined from them.The Squared Wasserstein Distance to a Fixed Measure: a One-Sided Bound Along Couplings, Differentiability at a Uniquely Mapped Source, and the Translation and Centring Identities
lemmalem:w2-squared-along-couplings-wasserstein-2026aAnalysisProbabilityThe squared Wasserstein distance to a fixed measure satisfies a one-sided quadratic bound along every coupling out of a mapped source, is differentiable along couplings with gradient twice the optimal displacement when the source is uniquely mapped, and transforms explicitly unde…Intrinsic Test Functions on the Wasserstein Space and Their Translation Hessians
definitiondef:intrinsic-test-function-wasserstein-2026cAnalysisProbabilityPDEA function on the Wasserstein space is an intrinsic test function on a set of measures when it is continuous, differentiable along couplings at each point of the set with a tangent gradient, its gradient is continuous along couplings of vanishing cost within the set, and it is tw…The Intrinsic Calculus on the Wasserstein Space: Standing Notation
settingset:wasserstein-intrinsic-2026bAnalysisProbabilityPDEStanding notation for the intrinsic theory of second-order equations on the Wasserstein space: couplings and the displacement pairing, optimal maps and the map property, differentiability along couplings, and the operator and penalty vocabulary. No probability space is assumed to…Two Sufficient Conditions for the Map Property: Absolute Continuity, and Atomlessness on the Line
lemmalem:map-property-sufficient-wasserstein-2026aAnalysisProbabilityA set of absolutely continuous measures has the map property in every dimension, and on the real line a set of atomless measures has it.The Map Property of a Set of Probability Measures
definitiondef:map-property-wasserstein-2026aAnalysisProbabilityA set of measures has the map property if every pair with a source in the set is uniquely mapped and the optimal displacement out of the source is tangent.Differentiability of a Function on the Wasserstein Space Along Couplings, and Its Gradient
definitiondef:differentiable-along-couplings-wasserstein-2026aAnalysisProbabilityA function on the Wasserstein space is differentiable along couplings at a measure if its increment is the displacement pairing of a square-integrable vector field along every coupling of small cost, up to an error of smaller order; that field is the gradient.A Square-Integrable Vector Field Whose Displacement Pairings Vanish to First Order is Zero
lemmalem:coupling-derivative-unique-wasserstein-2026aAnalysisProbabilityIf the displacement pairings of a square-integrable vector field along all couplings of small cost are of smaller order than the square root of the cost, the field is zero. This is what makes a gradient along couplings unique.