Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…Classical Sub- and Supersolutions of a Second-Order Equation on the Wasserstein Space
definitiondef:classical-sub-supersolution-wasserstein-2026cAnalysisProbabilityAn intrinsic test function on a set of measures is a classical subsolution, supersolution or solution of a second-order equation operator there when the operator, evaluated at the measure together with the value, the gradient along couplings and the translation Hessian of the fun…Degenerate Elliptic Second-Order Equation Operators on the Wasserstein Space
definitiondef:degenerate-elliptic-wasserstein-2026aAnalysisProbabilityA second-order equation operator on the Wasserstein space is degenerate elliptic when it is nonincreasing in its matrix argument for the positive semidefinite order.Basic Properties of the Delta-Envelopes on the Wasserstein Space
lemmalem:delta-envelopes-basic-wasserstein-2026bAnalysisProbabilityThe minus delta-envelope is upper semicontinuous and dominates the penalised function, and the plus envelope is dually placed; subordinate growth and the envelopes pass to the negative of a function with the two sides exchanged; for a continuous function and a lower semicontinuou…First- and Second-Order Conditions at a Penalised Extremum of a Test Function on the Wasserstein Space
lemmalem:penalised-maximiser-wasserstein-2026aAnalysisProbabilityAt a point of the score domain at which a test function minus a positive multiple of the penalty has a local maximum on the penalty domain, the intrinsic gradient equals that multiple of the score and the translation Hessian is negative semidefinite; the mirror statement holds at…First Variations of a Test Function on the Wasserstein Space Along Gradient Displacements and Along Translations
lemmalem:test-function-first-variation-wasserstein-2026aAnalysisProbabilityA translation moves a measure a Wasserstein distance at most the length of the shift. Along a displacement by the gradient of a compactly supported smooth function a test function is differentiable at time zero, with derivative the pairing of its intrinsic gradient with that grad…Sums, Real Multiples and Differences of Test Functions on the Wasserstein Space
lemmalem:test-function-wasserstein-linear-2026aAnalysisProbabilitySums, real multiples and differences of test functions on the Wasserstein space are again test functions, and the intrinsic gradient and the translation Hessian depend linearly on the test function.The Discrepancy of Two Square-Integrable Vector Fields Along a Coupling of Their Base Measures
lemmalem:coupling-field-distance-wasserstein-2026aAnalysisProbabilityFor a coupling of two measures with finite second moment and square-integrable vector fields against each of them, the integral of the squared distance between the two fields evaluated at the two coordinates is a finite nonnegative number independent of the representatives; along…The Score of a Penalty Pair is Determined by the Penalty
lemmalem:penalty-pair-score-unique-2026cAnalysisProbabilityAt each point of the score domain, the score of a penalty pair is the only tangent vector whose inner products with gradients of test functions are the first variations of the penalty; hence two penalty pairs with the same domains and the same penalty have the same score.The Push-Forward of a Probability Measure with Finite Second Moment by the Identity Perturbed along the Gradient of a Test Function: Borel, Finite Second Moment, the Diagonal Coupling and the Wasserstein Bound
lemmalem:gradient-push-forward-wasserstein-2026aAnalysisProbabilityFor a probability measure with finite second moment and a test function, the push-forward by the identity plus a multiple of the gradient is again a measure with finite second moment, at Wasserstein distance at most the multiple times the L^2-norm of the gradient; this is the def…The Dyson Hamilton-Jacobi Equation with Common Noise on the Wasserstein Space of the Real Line
equationeq:dyson-hamilton-jacobi-wasserstein-2026cAnalysisProbabilityThe Dyson Hamilton-Jacobi equation with common noise on the Wasserstein space of the real line, posed over the measures of finite free Fisher information: discount times the value, minus half the common-noise intensity times the trace of the matrix, plus half the squared norm of…The Discounted Hamilton-Jacobi Equation with Common Noise and Score Drift on the Wasserstein Space
equationeq:hamilton-jacobi-score-drift-wasserstein-2026cAnalysisProbabilityThe discounted Hamilton-Jacobi equation with common noise and score drift on the Wasserstein space, posed over the measures of finite Fisher information: discount times the value, minus half the common-noise intensity times the trace of the matrix, plus half the control cost time…