Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Penalty-Subordinate Growth of a Function on an Open Subset of Euclidean Space
definitiondef:penalty-subordinate-growth-euclidean-2026aAnalysisPDEA function on the domain of a penalty P has P-subordinate growth from above (below) if for every positive delta it is bounded above (below) by a constant plus (minus) delta times P.Basic Properties of the Sublevel Sets of a Penalty
lemmalem:penalty-open-set-basic-euclidean-2026aAnalysisPDEA penalty is bounded below; each strict sublevel set is a bounded open set whose closure is compact and lies in the closed sublevel set, and the penalty equals the level on its boundary.Penalty on an Open Subset of Euclidean Space
definitiondef:penalty-open-set-euclidean-2026aAnalysisPDEA penalty on an open subset D of Euclidean space is a real function of class C^2 on D all of whose sublevel sets are compact.Vector Fields with Test-Function Components are Dense in the Square-Integrable Vector Fields Against a Measure of Finite Second Moment
lemmalem:test-fields-dense-l2-euclidean-2026aAnalysisProbabilityVector fields whose components are smooth and compactly supported are dense in the square-integrable vector fields against any probability measure of finite second moment.Well-Posedness of the Hamilton-Jacobi Equation with Common Noise for Controlled Langevin Dynamics: Existence and Uniqueness of a Bounded Viscosity Solution
theoremthm:langevin-common-noise-well-posed-wasserstein-2026bAnalysisProbabilityPDEFor a confining potential, positive noise, control cost at most one, any common-noise matrix and a bounded uniformly continuous running cost, the Hamilton-Jacobi equation with common noise for controlled Langevin dynamics satisfies comparison for bounded sub- and supersolutions a…The Hamilton-Jacobi Equation with Common Noise for Controlled Langevin Dynamics in a Confining Potential on the Wasserstein Space
equationeq:langevin-common-noise-hamilton-jacobi-wasserstein-2026bAnalysisProbabilityPDEThe discounted Hamilton-Jacobi equation with common noise for controlled Langevin dynamics in a confining potential: the penalty-drift equation of the Langevin free-energy pair, whose drift is grad V plus sigma^2/2 times the score of the measure.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…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.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.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.Basic Properties of a Confining Potential on Euclidean Space: Continuity, Quadratic Minorants, the Tangent Inequality, Hessian Bounds, Growth under Translation, and Integrability
lemmalem:confining-potential-basic-euclidean-2026aAnalysisElementary properties of a confining potential V: continuity of V and its derivatives, quadratic lower bounds, the convexity tangent inequality, nonnegative Hessian with second derivatives bounded by the Laplacian, exponential control of V under translation, and integrability of…- A confining potential on R^d is a convex C^2 function with superquadratic growth, gradient bounded by a multiple of 1+|V|, and Laplacian small relative to |V|.
Change of Variables for the Lebesgue Integral under a Continuously Differentiable Bijection of Euclidean Space with Symmetric Positive Definite Jacobian Matrix, and the Density of a Push-Forward
theoremthm:change-of-variables-diffeomorphism-euclidean-2026aAnalysisMultivariable CalculusFor a bijection F of Euclidean space whose components and inverse components are continuously differentiable, with symmetric positive definite Jacobian matrix, the integral of f equals the integral of (f composed with F) times det DF for every nonnegative or integrable Borel f, a…