Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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|.
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.The Gradient of a Twice Continuously Differentiable Function with Hessian Pinched between Two Positive Multiples of the Identity is a Bi-Lipschitz Bijection of Euclidean Space with Continuously Differentiable Inverse
lemmalem:gradient-diffeomorphism-strongly-convex-2026aMultivariable CalculusFor a C^2 function whose Hessian is pinched between epsilon and L times the identity, the gradient map is a bi-Lipschitz bijection of Euclidean space whose inverse has C^1 components, with Jacobian matrix the inverse of the Hessian.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…Determinants of Positive Definite Matrices: Positivity, the Bound , Bounds under Pinching, and the Expansion of
lemmalem:log-determinant-bounds-2026aLinear AlgebraA symmetric positive definite d x d matrix A has positive determinant with log det A <= tr A - d. If epsilon I <= A <= L I, then A is positive definite and d - d/epsilon <= log det A <= dL - d. For a matrix B with entries bounded by m and |t| m small, det(I+tB) equals 1 + t tr B,…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 Uniqueness of Densities
theoremthm:radon-nikodym-sigma-finite-2026bAnalysisProbabilityFor a σ-finite measure μ, two integrable, or two nonnegative, functions with the same integrals over every measurable set agree outside a measurable μ-null set; and, under dependent choice, every finite measure and every finite signed measure that is absolutely continuous with re…The Function : Continuity, Young's Inequality and Lower Bounds, with the Elementary Bounds for the Exponential and the Logarithm
lemmalem:entropy-function-real-2026aAnalysisElementary bounds exp(u) >= 1+u and 1-1/t <= log t <= t-1, together with properties of the entropy function phi(s) = s log s on [0,infinity) (with phi(0)=0). The function phi is continuous, so phi of a nonnegative measurable function is measurable. It satisfies Young's inequality…A Confining Potential and Its Derivative are Continuous and Borel
lemmalem:confining-potential-basic-line-2026aAnalysisA confining potential on the real line and its derivative are continuous, hence Borel.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.Well-Posedness of the Dyson Hamilton-Jacobi Equation with Common Noise and a Confining Potential: Existence and Uniqueness of a Bounded Viscosity Solution
theoremthm:dyson-confined-well-posed-wasserstein-2026bAnalysisProbabilityPDEFor a confining potential and a bounded uniformly continuous running cost, the Dyson Hamilton-Jacobi equation with common noise satisfies comparison for bounded sub- and supersolutions and has exactly one bounded viscosity solution, which lies between plus and minus the cost boun…The Dyson Hamilton-Jacobi Equation with Common Noise and a Confining Potential on the Wasserstein Space of the Real Line
equationeq:dyson-confined-hamilton-jacobi-wasserstein-2026bAnalysisProbabilityPDEThe discounted Dyson Hamilton-Jacobi equation with common noise and a confining potential V on the Wasserstein space of the real line, the penalty-drift equation of the confined logarithmic-energy pair with unit control cost.The Hamilton-Jacobi Operator with Common Noise and Penalty Drift Satisfies the Hypotheses of the Comparison Principle for a Displacement Convex Pair
lemmalem:penalty-drift-comparison-hypotheses-wasserstein-2026cAnalysisProbabilityPDEFor a displacement convex penalty pair whose penalty controls the second moment and the common-noise contraction of the translation Hessian, control cost at most one and a bounded uniformly continuous running cost, the Hamilton-Jacobi operator with common noise along a matrix and…The Confined Logarithmic-Energy Pair is a Displacement Convex, Wasserstein-Coercive Penalty Pair with Closed Score and Regular Penalised Maxima
lemmalem:confined-log-energy-pair-properties-line-2026bAnalysisProbabilityThe confined logarithmic-energy pair is a Wasserstein-coercive, displacement convex penalty pair with closed score and regular penalised maxima, whose domain has the map property; its penalty is lower semicontinuous and controls the second moment and the translation Hessian, whic…The Confined Logarithmic-Energy Pair on the Wasserstein Space of the Real Line
definitiondef:confined-log-energy-pair-line-2026bAnalysisProbabilityThe confined logarithmic-energy pair on the real line: penalty a quarter of the inverse temperature times the logarithmic energy plus the integral of a confining potential V, with score V' minus a quarter of the inverse temperature times the free score.Splitting a Bounded First Variation into a Square-Integrable Potential Force and a Finite Free Fisher Information
lemmalem:confined-score-splitting-line-2026aAnalysisProbabilityFor a confining potential V and an atomless measure of finite logarithmic energy, if the first variation of V minus a multiple of the logarithmic energy is bounded in L^2, then V' is square-integrable and the measure has finite free Fisher information.