Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Square-Integrable Vector Fields Against a Probability Measure on Euclidean Space, and Test Functions: Standing Notation
settingset:wasserstein-tangent-2026aAnalysisProbabilityStanding notation for the space L^2(mu;R^d) of square-integrable vector fields on R^d with respect to a Borel probability measure mu, read as the space of square-integrable random vectors on the probability space (R^d, B(R^d), mu), with its inner product, norm, distance, closures…The Gradient of a Test Function is Bounded and Square-Integrable, and Its Laplacian Bounded and Integrable, Against Every Probability Measure
lemmalem:test-function-gradient-integrable-2026aAnalysisProbabilityFor a test function, each partial derivative and the Laplacian are continuous, compactly supported and bounded, so the gradient is a bounded Borel vector field whose squared norm is integrable against every Borel probability measure, and the Laplacian is integrable against every…Test Functions on Euclidean Space, Their Gradient Maps and Laplacians
definitiondef:test-function-euclidean-2026aAnalysisMultivariable CalculusA test function on R^q is a smooth, compactly supported real-valued function; the set of test functions is written C_c^infty(R^q). The gradient map of a test function sends x to the gradient at x, and its Laplacian is the Laplacian of a C^2 function.Existence of a Smooth Plateau Function on Euclidean Space
lemmalem:smooth-plateau-euclidean-2026aAnalysisMultivariable CalculusFor a centre x0 and radii r < s there is a smooth function on R^q with values in [0,1] that equals 1 on the closed ball of radius r about x0 and vanishes wherever the distance to x0 is at least s. This is the bump-function lemma restated for the current (recursive C^k) notion of…The Difference Quotient of a Function with Bounded Continuous Derivative is Bounded, Symmetric and Continuous on the Plane
lemmalem:difference-quotient-c1-real-2026aAnalysisFor a real function with bounded continuous derivative, the difference quotient extended to the diagonal by the derivative is bounded by the same bound, symmetric, continuous on the plane and hence Borel measurable.Scaled Cutoffs and the Second-Moment Test Functions: Uniform Derivative Bounds and Agreement on a Ball
lemmalem:cutoff-second-moment-test-functions-2026aAnalysisMultivariable CalculusRescaling a smooth bump function by a radius R gives smooth compactly supported cutoffs whose first and second partial derivatives are bounded by constants times 1/R and 1/R^2; multiplying the cutoff by half the squared norm gives smooth compactly supported functions whose gradie…Integration by Parts on Euclidean Space Against a Compactly Supported Function of Class
lemmalem:integration-by-parts-euclidean-2026aAnalysisMultivariable CalculusThe partial derivative of a compactly supported C^1 function on R^q integrates to zero, and consequently the integral of f times a partial derivative of g equals minus the integral of the same partial derivative of f times g whenever f and g are of class C^1 and g is compactly su…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.- A probability space is rich if every Borel probability measure on every Euclidean space is the law of some random vector on it.