Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.The Area Inequality for the Gradient of a Convex Function
theoremthm:area-inequality-convex-gradient-rn-2026aAnalysisFor a convex function and any nonnegative Borel h, the integral of h composed with the gradient, weighted by the determinant of the pointwise Hessian over points of twice differentiability, is at most the integral of h.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.Hessians of Two Convex Functions with Mutually Inverse Subgradients are Inverse Matrices at a Density Point
lemmalem:inverse-hessians-inverse-subgradients-rn-2026aAnalysisIf two convex functions have mutually inverse subgradients on a set, and each is twice differentiable at corresponding points, one of which is a density point of the set, then their Hessians there are positive definite and inverse to each other.Mollification at a Point of Twice Differentiability: Convergence of the Mollified Gradient and Hessian, and a Hessian Bound for Lipschitz Functions
lemmalem:mollified-derivatives-twice-differentiable-point-rn-2026aAnalysisMollifying a continuous function, the gradients and Hessians of the mollifications converge at every point where the function is twice differentiable; for a Lipschitz function the mollified Hessian is bounded by a constant times L over the mollification scale.The Points of Twice Differentiability of a Convex Function: a Borel Set of Full Measure, and Borel Measurability of the Gradient and Hessian on It
lemmalem:borel-second-derivatives-convex-rn-2026aAnalysisA convex function on an open convex set is twice differentiable on a Borel set of full measure, and on any Borel set of twice-differentiability points its gradient, Hessian entries, Hessian determinant and trace (extended by zero) are Borel, with nonnegative determinant and trace…Subgradients near a Point of Twice Differentiability of a Convex Function, and Invariance of the Second-Order Expansion under Lipschitz Truncation
lemmalem:alexandrov-point-subgradients-rn-2026aAnalysisAt a point where a convex function is twice differentiable, its only subgradient is the gradient, nearby subgradients follow the Hessian to first order, and a Lipschitz truncation above the gradient's norm keeps the same second-order expansion.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.Approximation of a Twice Continuously Differentiable Function with Bounded First and Second Derivatives by Test Functions
lemmalem:test-function-approximation-bounded-c2-euclidean-2026aAnalysisA C^2 function on Euclidean space whose first and second partial derivatives are bounded is the limit of a sequence of test functions whose first and second partial derivatives are uniformly bounded and converge pointwise to those of the function.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.A Continuously Differentiable Map Whose Jacobian Matrix is Close to the Identity Maps a Cube into a Slightly Larger Cube
lemmalem:near-identity-cube-2026aMultivariable CalculusIf every entry of the Jacobian matrix of a C^1 map differs from the identity by at most eta/d on a closed cube of half-side r, the map sends the cube into the cube about the image of the centre with half-side (1+eta)r.Lebesgue Measure under a Triangular or Symmetric Positive Definite Linear Map
lemmalem:lebesgue-linear-image-spd-2026aAnalysisLinear AlgebraLinear maps of Euclidean space are Borel, and Lebesgue integrals transform by the determinant under triangular matrices with positive diagonal and under symmetric positive definite matrices; in particular such a matrix multiplies Lebesgue measure by its determinant.