Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Law of Large Numbers for Empirical Measures is Uniform on Wasserstein-Compact Sets
corollarycor:empirical-measure-lln-uniform-wasserstein-2026aAnalysisProbabilityThe root-mean-square Wasserstein distance between the empirical measure of N samples and the sampled measure is 2-Lipschitz in the measure, uniformly in N, and therefore tends to zero uniformly over every compact set of measures.Law of Large Numbers for Empirical Measures in the Wasserstein Distance
theoremthm:empirical-measure-lln-wasserstein-2026aAnalysisProbabilityFor a probability measure with finite second moment, the root-mean-square Wasserstein distance between the empirical measure of N independent samples, drawn from the N-fold tensor power, and the measure itself tends to zero as N tends to infinity.The Mean-Square Norm of a Lipschitz Function Depends Lipschitz-Continuously on the Measure for the Wasserstein Distance
lemmalem:lipschitz-mean-square-wasserstein-2026aAnalysisProbabilityFor a Lipschitz function on Euclidean space with constant L, the square roots of the integrals of its square against two probability measures with finite second moment differ by at most L times their Wasserstein distance.Variance of the Empirical Mass of a Borel Set under a Tensor Power
lemmalem:empirical-cell-variance-euclidean-2026aAnalysisProbabilityUnder the N-fold tensor power of a probability measure, the empirical mass of a Borel set of mass c has mean-square deviation c(1-c)/N from c, and the square of its mean absolute deviation is at most c/N.The Wasserstein Distance between Two Probability Measures Carried by a Finite Set is Bounded by the Squared Diameter Times the Total Variation of the Masses
lemmalem:finite-support-wasserstein-euclidean-2026aAnalysisProbabilityIf two probability measures on Euclidean space are carried by the same finite set of points whose mutual distances are at most D, then their squared Wasserstein distance is at most D squared times the sum over the points of the absolute differences of their masses.Basic Properties of Empirical Measures: Values, Integrals, Push-Forwards, Second Moment, and Lipschitz Dependence on the Configuration
lemmalem:empirical-measure-basic-euclidean-2026aAnalysisProbabilityThe empirical measure of a configuration gives each Borel set the fraction of particles in it and integrates a function to its average over the particles; it commutes with product maps, has second moment the squared norm over N, depends Lipschitz-continuously on the configuration…The Empirical Measure of a Configuration of N Particles
definitiondef:empirical-measure-euclidean-2026aAnalysisProbabilityThe empirical measure of a configuration of N particles in Euclidean space is the one-particle marginal of the Dirac measure at the configuration, that is, the uniform average of the Dirac measures at the particles.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…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.