Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Convex Combinations of Probability Measures on Euclidean Space, and Finitely Supported Probability Measures as Combinations of Dirac Measures
lemmalem:convex-combination-measures-euclidean-2026aAnalysisProbabilityA convex combination of finitely many probability measures on Euclidean space is a probability measure whose integrals are the corresponding combinations of integrals, and a probability measure carried by finitely many distinct points is the combination of the Dirac measures at t…The Dirac Measure at a Point of Euclidean Space
definitiondef:dirac-measure-euclidean-2026aAnalysisProbabilityThe Dirac measure at a point of Euclidean space gives mass one to the Borel sets containing the point and mass zero to the others.Dirac Measures on Euclidean Space: Probability Measure, Integrals, Push-Forwards and the Coupling of Two Dirac Measures
lemmalem:dirac-measure-euclidean-2026aAnalysisProbabilityThe point mass at a point of Euclidean space is a probability measure with finite second moment equal to the squared norm of the point; it integrates every Borel function to its value at the point, is pushed forward to the point mass at the image, and two point masses are coupled…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…Lebesgue Measure on a Concatenated Euclidean Space: Iterated Integration over the Two Factors
lemmalem:lebesgue-concatenation-euclidean-2026aAnalysisThe Lebesgue integral of a nonnegative Borel function on R^{q+p} equals the iterated integral over R^q and R^p of its composition with the concatenation map.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…Particle Blocks: Linearity, Splitting of Inner Products, Product Maps and Diagonal Shifts
lemmalem:particle-blocks-basic-euclidean-2026aAnalysisBlock maps are linear and Borel, inner products and norms on R^{qN} split over the particles, product maps act blockwise and inherit measurability, continuity and Lipschitz bounds, and diagonal points shift every particle.Particle Blocks of the Configuration Space: Block Maps, Configurations, Product Maps and Diagonal Points
definitiondef:particle-blocks-euclidean-2026aAnalysisA point of R^{qN} is read as a configuration of N particles in R^q: the block maps extract the particles, configurations assemble them, product maps act particle by particle, and diagonal points repeat one particle.Lebesgue Measure on Euclidean Space is Sigma-Finite
lemmalem:lebesgue-measure-sigma-finite-euclidean-2026aAnalysisLebesgue measure on the Borel sets of R^q is sigma-finite: the open balls about the origin with natural radii are Borel, have finite measure, and cover R^q.- A convex Lipschitz integrand with constant L is a convex function on the nonnegative reals vanishing at zero that is nondecreasing and Lipschitz with constant L.
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.