Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Lift of the Second Moment: a Quadratic Function of Class with Gradient 2X and Translation Laplacian 2d
lemmalem:second-moment-lift-2026aAnalysisProbabilityThe lift of the second moment is the squared L^2 norm: a C^2 function on the space of square-integrable random vectors with gradient 2X, Hessian twice the identity form, and translation Laplacian 2d. This is the quadratic function in the explicit solution of the Dyson equation.The Lift of a Linear Functional of the Measure: Integrability, L-Gradient, Lipschitz Gradient Map and Translation Laplacian
lemmalem:linear-functional-lift-2026aAnalysisProbabilityFor a C^2 function f on R^d with bounded first and second partial derivatives, the functional u(mu) = integral of f against mu is defined on the Wasserstein space, its lift is U(X) = E f(X), u is continuously L-differentiable with L-gradient Df(X) and a Lipschitz gradient map, an…A Pair Maximising a Quadratically Penalised Difference of Law-Invariant Functions Within Its Laws Realises an Optimal Coupling
lemmalem:penalised-maximiser-optimal-coupling-2026aAnalysisProbabilityOn a rich probability space, if a pair of square-integrable random vectors maximises U(X) - V(Y) - alpha times the squared mean-square distance among pairs with the same laws, U and V law-invariant, then its mean-square distance equals the Wasserstein distance of the laws and the…Optimal Coupling of Two Probability Measures with Finite Second Moment
definitiondef:optimal-coupling-euclidean-2026aAnalysisProbabilityA coupling of two probability measures with finite second moment is optimal if its quadratic cost equals the square of their quadratic Wasserstein distance.The Translation Laplacian of a Function on the Space of Square-Integrable Random Vectors
definitiondef:translation-laplacian-lift-2026aAnalysisProbabilityA function on the space of square-integrable random vectors is twice continuously differentiable along translations at X if its restriction to the translates X plus a constant is of class C^2 in the constant; its translation Laplacian at X is the Laplacian of that restriction at…L-Differentiability of a Function on the Wasserstein Space via the Fréchet Derivative of Its Lift
definitiondef:l-differentiable-wasserstein-2026aAnalysisProbabilityA function on the quadratic Wasserstein space is L-differentiable if its lift is Fréchet differentiable on the Hilbert space of square-integrable random vectors, and continuously L-differentiable if the lift is of class C^1; the L-gradient at a random vector X is the gradient of…Basic Properties of the Lift: Law Invariance, the Correspondence on a Rich Space, and Transfer of Boundedness, Lipschitz Constants and Continuity
lemmalem:lift-basic-2026aAnalysisProbabilityThe lift of a function on the Wasserstein space is law-invariant; on a rich probability space lifting is a bijection onto the law-invariant functions; bounds, Lipschitz constants and uniform continuity transfer in both directions (the converses on a rich space), and continuity pa…The Lift of a Function on the Wasserstein Space to the Space of Square-Integrable Random Vectors
definitiondef:lift-wasserstein-function-2026aAnalysisProbabilityThe lift of a real function u on the quadratic Wasserstein space is the function X maps to u(law of X) on the space of square-integrable random vectors.Law-Invariant Function on the Space of Square-Integrable Random Vectors
definitiondef:law-invariant-function-2026aAnalysisProbabilityA real function on the space of square-integrable random vectors is law-invariant if it takes the same value at any two random vectors with the same law.The Wasserstein Space and Its Lift to Square-Integrable Random Vectors: Standing Notation
settingset:wasserstein-lift-2026aAnalysisProbabilityStanding notation for results on functions on the quadratic Wasserstein space and their lifts: a fixed dimension, a probability space (rich when a result cites that clause), the Hilbert space of square-integrable random vectors with its Fréchet calculus, the law map, the Wasserst…The Quadratic Wasserstein Distance is a Metric on the Wasserstein Space
theoremthm:wasserstein-metric-euclidean-2026aAnalysisProbabilityThe quadratic Wasserstein distance is symmetric, vanishes exactly on equal measures, and satisfies the triangle inequality, so it is a metric on the probability measures on R^d with finite second moment; the resulting metric space is the quadratic Wasserstein space.The Wasserstein Distance and the Mean-Square Distance of Random Vectors
lemmalem:wasserstein-lift-2026aAnalysisProbabilityThe law map from L^2(Omega;R^d) to P_2(R^d) is well defined and contracts the Wasserstein distance below the L^2 distance; on a rich probability space it is surjective and the Wasserstein distance is the infimum of the L^2 distance over random vectors with the prescribed laws.The Quadratic Wasserstein Distance on Euclidean Space
definitiondef:wasserstein-distance-euclidean-2026aAnalysisProbabilityThe quadratic Wasserstein distance between two probability measures on R^d with finite second moment is the square root of the infimum of the quadratic cost over all couplings.Couplings on Euclidean Space: Product Coupling, Swap, Finiteness of the Cost, Push-Forward Couplings, Modifying One Marginal, Quantisation, Gluing over a Finitely Supported Measure, and the Lipschitz Bound
lemmalem:coupling-toolkit-euclidean-2026aAnalysisProbabilityToolkit for couplings on R^d: the product coupling exists, the swap preserves the cost, the cost is finite for measures with finite second moment, push-forwards of a measure by a pair of Borel maps are couplings, one marginal can be modified by a Borel map at a Minkowski-type pri…The Space of Square-Integrable Random Vectors is a Real Hilbert Space; Its Laws Have Finite Second Moment; Constants and Translations
lemmalem:l2-random-vectors-hilbert-2026aAnalysisProbabilityL^2(Omega;R^d) is a real Hilbert space; the law of a square-integrable random vector has finite second moment equal to the squared L^2 norm; constant random vectors are square-integrable and translating a random vector pushes its law forward by the translation.The Space of Square-Integrable Random Vectors
definitiondef:l2-random-vectors-2026aAnalysisProbabilityThe space L^2(Omega;R^d) of classes, modulo almost sure equality, of square-integrable random vectors in R^d, with the inner product E[X.Y], its norm, and the law of a class.Square-Integrable Random Vectors: Coordinates, Operations, Almost Sure Equality and the Mean-Square Form
lemmalem:square-integrable-random-vectors-2026aAnalysisProbabilityA random vector has finite mean squared norm exactly when its coordinates are square-integrable; such vectors are closed under sums and scalar multiples, their dot products are integrable with a Cauchy-Schwarz bound, almost sure equality is an equivalence relation compatible with…Couplings of Two Probability Measures on Euclidean Space and Their Quadratic Cost
definitiondef:coupling-quadratic-cost-euclidean-2026aAnalysisProbabilityA coupling of two probability measures on R^d is a probability measure on R^{d+d} whose push-forwards by the two coordinate projections are the given measures; its quadratic cost is the integral of the squared distance between the two coordinates.The Second Moment of a Probability Measure on Euclidean Space and the Probability Measures with Finite Second Moment
definitiondef:wasserstein-space-p2-euclidean-2026aAnalysisProbabilityThe second moment of a Borel probability measure on R^d is the integral of the squared norm, and P_2(R^d) is the set of probability measures with finite second moment.Probability Measures on Euclidean Space and Random Vectors: Standing Notation
settingset:probability-measures-euclidean-2026aAnalysisProbabilityStanding notation for probability measures on Euclidean space and random vectors: Borel maps, the set of probability measures and their integrals, push-forwards, pairs of points with coordinate projections and product measures, and a probability space with expectations.