Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…Random Vectors: Coordinates, Functions, Pairs and Almost-Sure Equality
lemmalem:random-vector-basic-2026bProbabilityA function into R^n is a random vector exactly when its coordinates are random variables; measurable (in particular continuous) functions of random elements are random elements; the concatenation of two random vectors is a random vector; and almost surely equal random vectors hav…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.- A random vector in R^d is a measurable map from a probability space to R^d, with coordinates; its law is the image of the probability measure under it, a Borel probability measure on R^d.
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.Pairs of Euclidean Points: Coordinate Projections, Pairings, the Product Measure on a Euclidean Space, Borel Norm Functions and Finite Sets
lemmalem:euclidean-pairs-borel-toolkit-2026aAnalysisProbabilityToolkit for pairs of Euclidean points: the coordinate projections of a concatenated space are Borel, pairings of measurable maps are measurable, the product of two Borel probability measures transports to a probability measure on the concatenated space with the given marginals, t…The Hamilton-Jacobi Equation of the Controlled Heat Equation with Square-Integrable White Noise on the Torus
equationeq:hamilton-jacobi-white-noise-heat-torus-2026bAnalysisPDEThe discounted viscous Hamilton-Jacobi equation on the Sobolev space of order -(s+1) of the torus whose second-order term is the trace along the trigonometric white noise, whose Hamiltonian is half the squared norm of the gradient, and whose drift is minus the Laplacian, written…The Negative-Order Sobolev Triple of the Torus: a Diagonal Hilbert Triple whose Form Operator Is One Minus the Laplacian
lemmalem:sobolev-triple-white-noise-torus-2026aAnalysisThe Sobolev spaces of orders -(s+1) and -s on the torus form a Hilbert triple, which along any enumeration of the lattice is the diagonal triple of the rescaled trigonometric basis with the Fourier weights; the rescaled trigonometric classes are eigenvectors of the form operator…The Negative-Order Sobolev Spaces of the Torus are Hilbert Spaces: the Embedding of the Square-Integrable Classes, the Rescaled Trigonometric Basis, the Series Form of the Inner Product and the Inclusion of the Scale
lemmalem:negative-sobolev-space-torus-2026aAnalysisEach negative-order Sobolev space of the torus is a real Hilbert space isometric to the square-integrable classes through the realisation map; the Fourier coefficient families of square-integrable classes embed contractively; the realisation preimages of the trigonometric classes…The Negative-Order Sobolev Spaces of the Torus
definitiondef:negative-sobolev-space-torus-2026aAnalysisFor a natural number m, the Sobolev space of order -m on the torus is the space of coefficient families on the integer lattice whose rescaling by the m-th power of the inverse square roots of the Fourier weights is the Fourier coefficient family of a square-integrable class; its…Properties of the Fourier Coefficients on the Torus, and the Realisation of Weighted Coefficient Families
lemmalem:fourier-coefficients-torus-2026aAnalysisThe Fourier coefficient map is linear and injective, Parseval's identity and the Fourier expansion hold along any enumeration of the lattice, a square-summable coefficient family along an enumeration comes from exactly one class, and for each natural number m the families whose r…The Fourier Coefficients of a Square-Integrable Class on the Torus
definitiondef:fourier-coefficients-torus-2026aAnalysisThe Fourier coefficient family of a square-integrable class on the torus is the real-valued map on the integer lattice whose value at a lattice point is the inner product of the class with the corresponding trigonometric system class.Transport of an Inner Product and of Hilbert Space Structure along a Linear Bijection
lemmalem:hilbert-structure-transport-2026aAnalysisPulling an inner product back along a linear bijection from a real vector space onto a real inner product space yields an inner product for which the bijection is isometric; if the target is a Hilbert space so is the source, its inverse is linear, and orthonormal bases pull back…The Trigonometric System is an Orthonormal Basis of the Square-Integrable Space of the Torus
theoremthm:trigonometric-system-complete-torus-2026aAnalysisA square-integrable class on the torus that is orthogonal to every function of the trigonometric system is zero; consequently, enumerated along any bijection of the natural numbers with the integer lattice, the trigonometric system is an orthonormal basis of the square-integrable…Uniform Convergence of the Fejer Means of a Continuous Periodic Function on the Torus
lemmalem:fejer-mean-uniform-convergence-torus-2026aAnalysisThe Fejer means of a continuous lattice-periodic function converge to it uniformly on Euclidean space.