Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…Term-by-Term Differentiation of a Series of Continuously Differentiable Functions with Summable Uniform Bounds
lemmalem:series-c1-functions-euclidean-2026aAnalysisMultivariable CalculusA series of C^1 functions on R^q whose values and partial derivatives are dominated by summable constants converges to a C^1 function whose partial derivatives are the series of the partial derivatives, with the summed constants as bounds.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…The Gaussian Kernels on Euclidean Space: Scaling, Derivatives up to Order Three, the Convolution Identity, Moments and Tails
lemmalem:gaussian-kernel-euclidean-2026aAnalysisMultivariable CalculusFor 0<s<=1 the normalised Gaussian g_s on R^q scales as s^{-q/2}g_1(z/sqrt(s)), is smooth and even, has explicit partial derivatives up to order three with uniform and square-integral bounds of the expected powers of s, satisfies the convolution identity g_s*g_s=g_{2s}, has secon…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.The Viscosity Property on the Wasserstein Space Depends Only on the Values on the Penalty Domain
lemmalem:viscosity-domain-values-wasserstein-2026cAnalysisProbabilityTwo functions that agree on the penalty domain have the same delta-envelopes there, so one of them is a viscosity subsolution, supersolution or solution relative to the penalty pair exactly when the other is.The Hamilton-Jacobi Operator with Common Noise and Penalty Drift is Degenerate Elliptic
lemmalem:hamilton-jacobi-penalty-drift-elliptic-wasserstein-2026cAnalysisProbabilityThe Hamilton-Jacobi operator with common noise and penalty drift is degenerate elliptic, because the trace against the Gram product of the common-noise matrix is monotone for the positive semidefinite order.Classical Sub- and Supersolutions of a Degenerate Elliptic Equation on the Wasserstein Space are Viscosity Sub- and Supersolutions
propositionprop:classical-implies-viscosity-wasserstein-2026dAnalysisProbabilityFor a penalty pair with regular penalised maxima and a lower semicontinuous penalty, an intrinsic test function on the penalty domain with penalty-subordinate growth that is a classical subsolution or supersolution of a degenerate elliptic operator on the score domain is a viscos…Sign Reversal for Second-Order Equations on the Wasserstein Space: Subsolutions of F are Supersolutions of its Reversal
lemmalem:viscosity-sign-reversal-wasserstein-2026dAnalysisProbabilityReversing the signs of the value, the vector field and the matrix turns a second-order equation operator on the Wasserstein space into another one with the same ellipticity, exchanges its two delta-shifts, and exchanges classical and viscosity subsolutions with supersolutions of…