Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Intrinsic Test Functions at a Maximiser of the Doubled Difference Linked through Tensor Powers
lemmalem:tensor-doubling-test-functions-wasserstein-2026aAnalysisProbabilityAt a maximiser of a configuration-level envelope minus N times a particle-level envelope minus half a multiple of the squared distance from the configuration law to the tensor power, there is a maximising pair near which both envelopes are touched by intrinsic test functions whos…Existence, Penalty Bounds and Monotonicity of the Maximum of a Two-Space Doubled Difference with a Continuous Link
lemmalem:two-space-doubling-maximiser-wasserstein-2026aAnalysisProbabilityFor Wasserstein-coercive penalty pairs at the particle dimension or at the configuration level, a bounded-above function, a bounded-below function and a continuous nonnegative link, the weighted doubled difference of their delta-envelopes minus a multiple of the link attains its…Closure of Approximate Test Data for Viscosity Sub- and Supersolutions on the Wasserstein Space
lemmalem:viscosity-closure-wasserstein-2026aAnalysisProbabilityPDEIf a bounded viscosity subsolution (supersolution) is touched from above (below) by intrinsic test functions at points converging along couplings to a limit point, with gradients converging along those couplings to a field and translation Hessians converging to a matrix, then the…A Configuration-Level Majorant of the Distance from a One-Particle Marginal, Touching at a Given Configuration Law
lemmalem:marginal-distance-majorant-wasserstein-2026aAnalysisProbabilityPushing a configuration law forward by the product of an optimal map from its one-particle marginal to a target gives a configuration law whose squared distance majorises N times the squared distance of one-particle marginals to the target, with equality at the given law; the opt…Pulling Back Intrinsic Test Functions along Tensor Powers
lemmalem:tensor-pullback-test-function-wasserstein-2026aAnalysisProbabilityIf a function on the configuration-level Wasserstein space is an intrinsic test function on a set containing the tensor powers of a set of one-particle laws, then its composition with the tensor power is an intrinsic test function on that set; its gradient is N times the one-part…Classical Solutions of the N-Particle Hamilton-Jacobi Equation Lift to Classical Solutions of the Lifted Equation, and a Bounded One is the Lifted Viscosity Solution
theoremthm:n-particle-lift-classical-wasserstein-2026aAnalysisProbabilityPDEIf a function on the configuration space with bounded first and second derivatives is a classical sub- or supersolution of the N-particle Hamilton-Jacobi equation, then its integral against the measure is a classical sub- or supersolution of the lifted equation, the Laplacian of…Well-Posedness of the Lifted N-Particle Hamilton-Jacobi Equation: Comparison, Existence and Uniqueness of a Bounded Viscosity Solution
corollarycor:n-particle-lifted-well-posed-wasserstein-2026aAnalysisProbabilityPDEFor a confining potential, positive noise, control cost at most one, any common-noise matrix and a bounded uniformly continuous running cost on the configuration space, the lifted N-particle Hamilton-Jacobi equation satisfies comparison and has exactly one bounded viscosity solut…The Lifted N-Particle Hamilton-Jacobi Equation on the Wasserstein Space of the Configuration Space
equationeq:n-particle-lifted-hamilton-jacobi-wasserstein-2026aAnalysisProbabilityPDEThe lift of the N-particle Hamilton-Jacobi equation to probability measures on the configuration space: the Langevin Hamilton-Jacobi equation with common noise at the configuration level, with the N-particle potential, the N-particle common-noise matrix and the integral of the ru…The N-Particle Hamilton-Jacobi Equation with Individual and Common Noise on the Configuration Space
equationeq:n-particle-hamilton-jacobi-euclidean-2026aAnalysisProbabilityPDEThe discounted Hamilton-Jacobi equation on the configuration space of N particles in a confining potential: individual noise enters as the full Laplacian, common noise as the trace of the Hessian against the common-noise matrix whose rows move every particle by the same vector, w…Running Costs for N-Particle Systems: Integrals of Bounded Uniformly Continuous Functions and Costs of the Empirical Measure
lemmalem:n-particle-running-cost-wasserstein-2026aAnalysisProbabilityIntegrating a bounded uniformly continuous function against a measure gives a bounded uniformly continuous function on the Wasserstein space, with the same bound; and a bounded uniformly continuous function of the empirical measure of a configuration is a bounded uniformly contin…The N-Particle Potential of a Confining Potential is a Confining Potential on the Configuration Space
lemmalem:n-particle-potential-euclidean-2026aAnalysisProbabilitySumming a confining potential over the N particles of a configuration gives a twice continuously differentiable function on the configuration space whose gradient is the configuration of the particle gradients and whose Laplacian is the sum of the particle Laplacians, and this N-…Integrals of Functions with a Bounded Hessian are Intrinsic Test Functions on the Wasserstein Space
lemmalem:linear-functional-intrinsic-wasserstein-2026bAnalysisProbabilityFor a twice continuously differentiable function with bounded second derivatives, hence of at most quadratic growth, the integral of the function against a measure is an intrinsic test function on the whole Wasserstein space; its gradient along couplings is the gradient of the fu…N-Particle Systems on the Wasserstein Space: Particles, Configurations and the Configuration Level
settingset:n-particle-wasserstein-2026bAnalysisProbabilityStanding notation for systems of N particles in d-dimensional space: the configuration space of dimension dN with its block maps, tensor powers, one-particle marginals and empirical measures, and the convention that the Wasserstein results and notions, stated for an arbitrary dim…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.