Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.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 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.- A confining potential on the real line is a convex function of class C^2 that grows faster than every multiple of x^2, whose derivative is bounded by a multiple of one plus its absolute value, and whose second derivative is small against its absolute value.
Displacement Convexity of the Logarithmic Energy on the Real Line
lemmalem:logarithmic-energy-displacement-convex-line-2026aAnalysisProbabilityOn the real line the logarithmic energy lies above its tangent along optimal couplings: at a measure of finite free Fisher information, the energy plus the displacement pairing of minus the free score is at most the energy of the target.A Probability Measure on the Real Line with a Continuously Differentiable Density of Bounded Derivative Has Finite Free Fisher Information and Finite Logarithmic Energy
lemmalem:free-fisher-smooth-density-line-2026aAnalysisProbabilityA probability measure on the real line with finite second moment and a continuously differentiable density of bounded derivative has finite free Fisher information and finite logarithmic energy.The First Variation of the Logarithmic Energy on the Real Line along Gradient Perturbations of the Identity
lemmalem:logarithmic-energy-first-variation-line-2026aAnalysisProbabilityAlong the push-forward by the identity plus a small multiple of the derivative of a test function, the logarithmic energy is differentiable at zero with derivative minus the double integral of the difference quotient, which is minus the pairing with the free score when the free F…Basic Properties of the Logarithmic Energy on the Real Line: Lower Bound, Translation Invariance, Closed Sublevel Sets and Lower Semicontinuity
lemmalem:logarithmic-energy-basic-line-2026aAnalysisProbabilityThe logarithmic energy is bounded below by minus one minus the second moment, is invariant under translations, has sublevel sets closed under Wasserstein convergence, and is lower semicontinuous.The Logarithmic Energy of a Probability Measure on the Real Line
definitiondef:logarithmic-energy-line-2026aAnalysisProbabilityThe logarithmic energy of an atomless probability measure on the real line with finite second moment is the double integral of -log|x-y|, defined on the measures for which that kernel is integrable.Wasserstein Convergence from Weak Convergence with Uniformly Integrable Second Moments, and Wasserstein Compactness under a Superquadratic Moment Bound
lemmalem:w2-compactness-superquadratic-moment-euclidean-2026aAnalysisProbabilityWeak convergence together with uniformly integrable second moments gives convergence in the Wasserstein distance, and a uniform bound on a superquadratic moment gives a Wasserstein-convergent subsequence.Uniqueness and Continuity on Energy Sublevel Sets of Bounded Viscosity Solutions on the Wasserstein Space
corollarycor:comparison-uniqueness-continuity-wasserstein-2026bAnalysisProbabilityPDEUnder the hypotheses of the comparison principle, two bounded viscosity solutions coincide on the penalty domain, and a bounded viscosity solution is uniformly continuous in the Wasserstein distance on every sublevel set of the penalty.The Delta-Envelopes of Bounded Functions and Their Monotonicity in the Weight, for a Wasserstein-Closed Penalty Pair
lemmalem:delta-envelopes-bounded-wasserstein-2026bAnalysisProbabilityPDEFor a Wasserstein-closed penalty pair, a function bounded above on the penalty domain has penalty-subordinate growth from above and its delta-envelope lies below the bound minus delta times the penalty; and increasing the weight from delta to delta' lowers the upper envelope by a…