Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.Continuity, Semicontinuity and Lipschitz Bounds Pass from the Centred Heat Gauge to the Wasserstein Distance
lemmalem:gauge-continuity-comparison-wasserstein-2026aAnalysisProbabilityBecause the centred heat gauge is dominated by a constant multiple of the Wasserstein distance, a function continuous, upper or lower semicontinuous, or Lipschitz for the gauge is so for the Wasserstein distance.Coercive Penalty Pairs on the Wasserstein Space
definitiondef:coercive-penalty-pair-wasserstein-2026aAnalysisProbabilityA penalty pair is coercive when, for every level, the set of measures of the penalty domain at which the penalty does not exceed that level is sequentially compact for the centred heat gauge and has bounded second moments.The Convolution of a Bounded Continuous Function with a Probability Measure on Euclidean Space: Continuity, Boundedness and Differentiation Under the Integral
lemmalem:convolution-measure-c1-euclidean-2026aAnalysisProbabilityIntegrating a bounded continuous function of y-x against a probability measure in x gives a bounded continuous function of y; if the function is C^1 with bounded partial derivatives, the result is C^1 and its partial derivatives are obtained by differentiating under the integral.The Centred Heat Gauge: Metric Properties, Comparison with the Wasserstein Distance, Behaviour Under Translations, the Squared Gauge as a Test Function, and the Polarisation Inequality
lemmalem:centred-heat-gauge-wasserstein-2026aAnalysisProbabilityPDEThe centred heat gauge is a metric on the Wasserstein space dominated by a constant times W_2, is exactly quadratic along translations of either argument, and its square in one argument is a test function with an explicit gradient (a constant plus a bounded smooth field of size c…The Centred Heat Gauge on the Wasserstein Space
definitiondef:centred-heat-gauge-wasserstein-2026aAnalysisProbabilityThe centred heat gauge of two square-integrable probability measures is the square root of the squared Euclidean distance of their means plus the squared heat gauge of their centred versions.Linear and Quadratic Kernel Functionals of a Measure Are Test Functions on the Wasserstein Space
lemmalem:quadratic-kernel-functional-wasserstein-2026aAnalysisProbabilityFor f of class C^2 with bounded first and second derivatives, the linear functional mu -> int f dmu is a test function with gradient Df and translation Hessian the mean of D^2 f; for an even such kernel K, the quadratic functional mu -> iint K(x-y) dmu dmu is a translation-invari…The Mean of a Square-Integrable Probability Measure, Its Lift, Its Centring, and Functions of the Mean and Centred Integrals as Test Functions
lemmalem:mean-centring-wasserstein-2026aAnalysisProbabilityThe mean of a square-integrable measure is the expectation of any lift, is 1-Lipschitz for the Wasserstein distance and shifts under translations; the centred measure has mean zero, is translation invariant and 2-Lipschitz in W_2; a C^2 function of the mean is a test function wit…Gradients of Functions with Bounded Derivatives Belong to the Tangent Space; Constants Are Tangent; the Score Identity; the Score Has Mean Zero; Translation of Tangent Fields
lemmalem:bounded-gradient-tangent-wasserstein-2026aAnalysisProbabilityFor a C^1 function of linear growth with bounded gradient, the class of its gradient lies in the tangent space of the Wasserstein space at every square-integrable measure, in particular constant fields are tangent; for a C^2 function with bounded first and second derivatives the…The Heat Gauge on the Probability Measures on Euclidean Space
definitiondef:heat-gauge-euclidean-2026aAnalysisProbabilityThe heat gauge of two probability measures on R^q is the square root of the heat gauge form Q(mu,nu) built from the multiscale Gaussian kernel.A Probability Measure on Euclidean Space Is Determined by the Integrals of Lipschitz Functions with Values in the Unit Interval
lemmalem:measure-determined-by-lipschitz-functions-2026aAnalysisProbabilityTwo probability measures on R^q that give the same integral to every Lipschitz function with values in [0,1] are equal.The Heat Gauge Form on Probability Measures: Algebra, Representation by Smoothed Densities, Positivity, Cauchy-Schwarz, Separation, the Triangle Inequality, the Wasserstein Bound and Derivative Bounds for the Potential
lemmalem:heat-gauge-form-wasserstein-2026aAnalysisProbabilityThe bilinear form B built from the multiscale kernel pairing is represented as a sum over scales of Lebesgue integrals of products of differences of Gaussian smoothings; its quadratic form Q is nonnegative, satisfies Cauchy-Schwarz and the triangle inequality for its square root,…The Multiscale Gaussian Kernel: Definition by a Series, Regularity and Bounds, the Smoothed Potential of a Probability Measure and the Kernel Pairing of Two Measures
lemmalem:heat-kernel-series-euclidean-2026aAnalysisProbabilityThe kernel K=sum_k 2^{-k(q+8)} g_{2 4^{-k}} is an even C^3 function with bounded derivatives; K*nu is C^3 with derivatives under the integral; and the pairing of two probability measures through K equals the sum over scales of the Lebesgue integrals of products of Gaussian smooth…Gaussian Smoothing of a Probability Measure on Euclidean Space: Regularity, Mass, Duality, Approximation of a Bounded Function with a Modulus of Continuity, and the Pairing Identity
lemmalem:gaussian-smoothing-measure-euclidean-2026aAnalysisProbabilityThe Gaussian smoothing g_s*mu of a probability measure on R^q is a bounded C^3 density of mass one whose derivatives are obtained under the integral; integrating a bounded Borel function against it equals integrating the smoothed function against mu; smoothing approximates a func…Plans on the Product of a Euclidean Space with Itself
definitiondef:plan-wasserstein-2026aAnalysisProbabilityA plan in dimension d is a probability measure with finite second moment on the product of d-dimensional Euclidean space with itself.