Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Langevin Free-Energy Pair is a Wasserstein-Coercive Penalty Pair: Growth Bounds, Continuity of the Translation Hessian, and the First Variation of the Penalty
lemmalem:langevin-free-energy-penalty-pair-euclidean-2026bProbabilityThe Langevin free-energy pair is a Wasserstein-coercive penalty pair whose domain has the map property; its translation Hessian is the integral of the Hessian of V, the penalty is lower semicontinuous and controls the second moment and the trace of the translation Hessian, each e…The Langevin Free-Energy Pair of a Confining Potential on the Wasserstein Space
definitiondef:langevin-free-energy-pair-euclidean-2026aProbabilityFor a confining potential V and a noise intensity sigma, the penalty is the free energy of Langevin dynamics, sigma^2/2 times the entropy plus the potential energy, on measures of finite entropy integrating V; its score is grad V plus sigma^2/2 times the score of the measure, on…The Potential Energy of a Confining Potential: Smoothness in Translations, First Variation, Closed Sublevel Sets and Convergence at Bounded Energy
lemmalem:potential-energy-basic-euclidean-2026aAnalysisProbabilityFor a confining potential V, the potential energy of a measure is twice continuously differentiable in translations with Hessian the integral of the Hessian of V, has first variation the integral of grad V against the test gradient, has closed sublevel sets under Wasserstein conv…Radial Retraction onto a Closed Ball: Compactly Supported Approximation in the Wasserstein Distance
lemmalem:radial-retraction-wasserstein-euclidean-2026aProbabilityPushing a measure forward by the radial retraction onto a closed ball gives a measure carried by the ball, and for a measure of finite second moment these push-forwards converge to it in the Wasserstein distance as the radius grows.Convergence in the Wasserstein Distance Implies Weak Convergence and Convergence of Integrals of Continuous Functions of Quadratic Growth
lemmalem:wasserstein-convergence-weak-euclidean-2026aProbabilityIf measures of finite second moment converge in the Wasserstein distance, they converge weakly, and the integrals of every continuous function of at most quadratic growth converge.McCann's Tangent Inequality: the Entropy Lies Above its Tangent Along Optimal Maps
theoremthm:entropy-tangent-inequality-euclidean-2026aAnalysisProbabilityIf mu and nu have finite entropy, mu has finite Fisher information and T is the optimal map from mu to nu, then Ent(mu) plus the pairing of the score of mu with T minus the identity is at most Ent(nu): the entropy lies above its tangent along optimal maps.The Score Paired with the Identity, and the Laplacian of a Convex Potential Bounded by its Pairing with the Score
lemmalem:laplacian-score-comparison-convex-euclidean-2026aAnalysisProbabilityFor an absolutely continuous measure with finite Fisher information, the score paired with the identity is minus the dimension, and the integral of the pointwise Laplacian of a convex potential with square-integrable gradient is at most minus its pairing with the score.Along an Optimal Map between Absolutely Continuous Measures the Hessians of the Two Convex Potentials are Inverse Matrices
lemmalem:hessians-along-optimal-maps-euclidean-2026aAnalysisProbabilityFor the optimal maps between two absolutely continuous measures with finite second moment and their convex potentials, almost every point is one where both potentials are twice differentiable along the map, with positive definite, mutually inverse Hessians.Splitting a Bounded First Variation into a Square-Integrable Potential Force and a Finite Fisher Information
lemmalem:confining-score-splitting-euclidean-2026aProbabilityFor a confining potential V and a measure integrating V, if the combined first variation of the potential energy and a multiple of the entropy is bounded by the L^2 norm of the test gradient, then the force of V is square-integrable and the measure has finite Fisher information.The Score Integrates by Parts Against Every Compactly Supported Continuously Differentiable Vector Field
lemmalem:score-integration-by-parts-fields-euclidean-2026aProbabilityThe score of a measure of finite Fisher information, defined by testing against gradients only, satisfies the integration-by-parts identity against every compactly supported C^1 vector field: its pairing with the field is minus the mean of the divergence.Gaussian Smoothing of a Measure with Finite Second Moment: Positive Density, Finite Entropy, a Tangent Score, Non-Increasing Fisher Information and Exponential Integrability
lemmalem:gaussian-smoothing-entropy-score-euclidean-2026aProbabilityThe Gaussian smoothing of a measure with finite second moment has a positive C^2 density, finite entropy and finite Fisher information, lies within W_2-distance sqrt(ds) of the measure, and its score is the logarithmic gradient of the density, a tangent field because the density…The Gradient of a Convex Continuously Differentiable Function Belongs to the Tangent Space When It Is Square-Integrable
lemmalem:convex-gradient-tangent-wasserstein-2026aProbabilityIf a convex function of class C^1 on Euclidean space has a gradient that is square-integrable against a measure of finite second moment, that gradient lies in the tangent space of the Wasserstein space at the measure.The First Variation of the Entropy Along a Gradient Perturbation of the Identity
lemmalem:entropy-first-variation-euclidean-2026aProbabilityPushing a measure of finite entropy forward by the identity plus a small multiple of the gradient of a test function keeps the entropy finite, changes it by minus the mean of log det of the perturbed Hessian, and the derivative at zero is minus the mean of the Laplacian.The Entropy of the Push-Forward of a Measure by the Gradient of a Twice Continuously Differentiable Function with Pinched Hessian
lemmalem:entropy-pushforward-gradient-map-2026aProbabilityPushing a measure with finite entropy and second moment forward by the gradient of a twice continuously differentiable function whose Hessian is pinched between two positive multiples of the identity keeps both finite, and lowers the entropy by the mean of log det of the Hessian.Basic Properties of the Entropy on the Wasserstein Space: Comparison with the Gaussian Relative Entropy, Lower Bound, Translation Invariance, Absolute Continuity, Closed Sublevel Sets and Lower Semicontinuity
lemmalem:entropy-basic-euclidean-2026aProbabilityThe entropy of a measure with finite second moment equals its relative entropy with respect to the standard Gaussian plus log c_1 minus half the second moment. Consequences: the entropy is bounded below, invariant under translations, finite only for absolutely continuous measures…The Entropy of a Probability Measure on Euclidean Space
definitiondef:entropy-euclidean-2026aAnalysisProbabilityA probability measure on R^d has finite entropy if it has a Lebesgue density rho with rho log rho integrable; its entropy is the integral of rho log rho. P_2^Ent is the set of such measures with finite second moment.Relative Entropy on Euclidean Space: the Gibbs Inequality, a Variational Criterion for Finite Relative Entropy, and Closed Sublevel Sets under Weak Convergence
lemmalem:relative-entropy-gibbs-closed-2026aProbabilityFor probability measures on R^m, relative entropy dominates the Donsker-Varadhan functional int h dnu - log int e^h dgamma for bounded Borel h (Gibbs inequality); conversely a uniform bound on this functional over bounded Lipschitz h implies finite relative entropy with the same…- A probability measure has finite relative entropy with respect to another if it has a density f with f log f integrable; the relative entropy is the integral of f log f.
The Radon-Nikodym Theorem for a Finite Measure and a Sigma-Finite Measure, and Uniqueness of Densities
theoremthm:radon-nikodym-sigma-finite-2026aAnalysisProbabilityDensities of a finite measure with respect to any measure are integrable and unique up to a null set; and a finite measure that vanishes on the null sets of a sigma-finite measure has a density with respect to it (Radon-Nikodym).The Logarithmic Kernel on the Real Line: Borel Measurability, a Linear Lower Bound, and the Null Diagonal of an Atomless Measure
lemmalem:logarithmic-kernel-line-2026aAnalysisProbabilityThe logarithmic kernel -log|x-y|, set to zero on the diagonal, is Borel and bounded below by -|x|-|y|, and the diagonal is null for the product of an atomless measure with itself.