Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Scores on the Configuration Space: the Score of a Tensor Power is the Product Field of the Score, and the Score of the One-Particle Marginal is the Projection of the Score
lemmalem:score-tensor-marginal-wasserstein-2026aAnalysisProbabilityA tensor power of a measure with finite Fisher information has finite Fisher information, with the product field of the score as its score and N times the Fisher information; and the one-particle marginal of a measure on R^{dN} with finite Fisher information has as score the one-…Entropy on the Configuration Space: Tensorization, Subadditivity over the Particles, and the One-Particle Marginal
lemmalem:entropy-tensor-marginal-euclidean-2026aAnalysisProbabilityThe entropy of an N-th tensor power is N times the entropy of the factor; the entropies of the N particle laws of a measure on R^{qN} add up to at most its entropy; and N times the entropy of the one-particle marginal is at most the entropy of the measure.Entropy of Products, Subadditivity over Two Marginals, and Convexity of the Entropy
lemmalem:entropy-product-marginals-euclidean-2026aAnalysisProbabilityThe entropy of a product of two measures with finite entropy is the sum of their entropies; a measure on a concatenated space with finite entropy and finite second moment has marginals of finite entropy whose entropies add up to at most its own; and the entropy is convex under fi…Tensor Powers Scale the Wasserstein Distance by the Square Root of N, and the One-Particle Marginal is Lipschitz with Constant
lemmalem:tensor-marginal-wasserstein-2026aAnalysisProbabilityThe squared Wasserstein distance between N-th tensor powers is N times that between the factors, and the squared distance between one-particle marginals is at most 1/N times that between the measures on the configuration space.The Projection onto One-Particle Tangent Fields: Pairing with Product Fields, Contraction, and Product Fields of Tangent Fields
lemmalem:product-field-projection-properties-wasserstein-2026aAnalysisProbabilityThe projection represents the pairing of a field with every product field of a tangent field, is a contraction up to the factor N^{-1/2}, is linear, and returns g when applied to the product field of a tangent field g.Product Fields and the Projection onto One-Particle Tangent Fields
definitiondef:product-field-projection-wasserstein-2026aAnalysisProbabilityFor a measure P on R^{dN} with finite second moment, a square-integrable field g on its one-particle marginal acts on every particle to give the product field on P; and a square-integrable field D on P projects to the tangent field on the one-particle marginal representing its pa…Tensor Powers and One-Particle Marginals: Particle Laws, Product Integrals, Push-Forwards, Moments, Product Maps and Diagonal Shifts
lemmalem:tensor-marginal-properties-euclidean-2026aProbabilityUnder a tensor power each particle has the factor law and any two particles are independent; tensor powers commute with product maps and diagonal shifts; the one-particle marginal of a tensor power is the factor; second moments scale by N; and product maps integrate against a mea…The One-Particle Marginal of a Probability Measure on the Configuration Space
definitiondef:one-particle-marginal-euclidean-2026aProbabilityThe one-particle marginal of a probability measure on R^{qN} is the average of the laws of its N particles, a probability measure on R^q.The Tensor Power of a Probability Measure on Euclidean Space
definitiondef:tensor-power-probability-euclidean-2026aProbabilityThe N-th tensor power of a probability measure on R^q is the probability measure on R^{qN} under which the N particles are independent with that law.Existence and Uniqueness of Tensor Powers, and the Average of the Block Marginals
lemmalem:tensor-power-marginal-average-euclidean-2026aProbabilityFor a probability measure on R^q there is exactly one probability measure on R^{qN} giving each block rectangle the product of the factor masses; and for a probability measure on R^{qN} the average of its N block marginals is a probability measure on R^q integrating by averaging.Well-Posedness of the Langevin Hamilton-Jacobi Equation with Common Noise and a Density Cost: Existence and Uniqueness of a Bounded Viscosity Solution
theoremthm:langevin-density-cost-well-posed-wasserstein-2026bAnalysisProbabilityPDEFor a confining potential, positive noise, a common-noise matrix, control cost at most one, a bounded uniformly continuous running cost and the density cost of a convex Lipschitz integrand, in any dimension, the Langevin Hamilton-Jacobi equation with common noise and density cost…The Langevin Hamilton-Jacobi Operator with a Density Cost Satisfies the Hypotheses of the Comparison Principle and of Perron's Method
lemmalem:langevin-density-cost-comparison-hypotheses-wasserstein-2026cAnalysisProbabilityPDEFor a confining potential, positive noise, a common-noise matrix, control cost at most one, a bounded uniformly continuous running cost and the density cost of a convex Lipschitz integrand, the Langevin Hamilton-Jacobi operator with common noise and density cost is degenerate ell…The Langevin Hamilton-Jacobi Equation with Common Noise and a Density Cost on the Wasserstein Space
equationeq:langevin-density-cost-hamilton-jacobi-wasserstein-2026bAnalysisProbabilityPDEThe Langevin Hamilton-Jacobi equation in a confining potential with common noise along a common-noise matrix, with the density cost of a convex Lipschitz integrand added to the running cost.The Density Cost Along Optimal Maps is Controlled by the Monotonicity of the Score
lemmalem:density-cost-optimal-maps-euclidean-2026bAnalysisProbabilityFor two absolutely continuous measures with finite Fisher information and the optimal maps between them, the difference of their density costs is at most any positive multiple A of the sum of the pairings of the scores with the two optimal displacements, plus the dimension times…McCann's Jacobian Equation Along an Optimal Map Between Absolutely Continuous Measures
lemmalem:jacobian-equation-optimal-map-euclidean-2026aAnalysisProbabilityAlong the optimal map between two absolutely continuous measures with finite second moment, the density of the source equals the density of the target at the image point times the determinant of the Hessian of the convex potential, almost everywhere for the source.The Density Cost of a Convex Lipschitz Integrand
definitiondef:density-cost-euclidean-2026bAnalysisProbabilityThe density cost of a convex Lipschitz integrand assigns to an absolutely continuous probability measure with finite second moment the Lebesgue integral of the integrand composed with its density; it lies between zero and the Lipschitz constant.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 Langevin Free-Energy Pair is Displacement Convex, with Closed Score Along Couplings and Regular Penalised Maxima
lemmalem:langevin-free-energy-pair-regularity-euclidean-2026aProbabilityThe Langevin free-energy pair has closed score along couplings and regular penalised maxima, and it is displacement convex.