Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Noise Wasserstein Distance is a Metric on the Measures Noise-Connected to the Reference Measure: Existence of Noise-Optimal Couplings, Comparison with the Quadratic Wasserstein Distance and Lower Semicontinuity
theoremthm:noise-wasserstein-metric-hilbert-2026aAnalysisProbabilityThe measures noise-connected to the reference measure have finite second moment and are pairwise noise-connected, noise-optimal couplings exist, and the noise Wasserstein distance is a metric on them that dominates the quadratic Wasserstein distance up to a constant and is lower…The Noise Wasserstein Distance
definitiondef:noise-wasserstein-distance-hilbert-2026aAnalysisProbabilityThe noise Wasserstein distance between two noise-connected measures is the square root of the least noise cost of their couplings of finite noise cost; a coupling attaining it is noise-optimal. The measures noise-connected to the reference measure form the set on which this dista…The Noise Gradient of a Cylindrical Function and the Noise Tangent Space at a Probability Measure on a Hilbert Space
definitiondef:noise-tangent-space-hilbert-2026aAnalysisProbabilityDefines the noise gradient of a bounded C^1 cylindrical function, a bounded measurable map into the noise space, and the noise tangent space at a probability measure as the closure of the noise gradients in the square-integrable noise fields.Gluing Two Couplings on a Hilbert Space over a Common Middle Marginal, and the Triangle Inequalities for the Quadratic and Noise Costs
lemmalem:gluing-couplings-hilbert-2026aAnalysisProbabilityTwo couplings on a Hilbert space sharing a middle marginal can be glued into a probability measure on the threefold product; the composite coupling of the outer marginals satisfies the triangle inequality for the square roots of the quadratic cost and, for couplings of finite noi…Couplings of Finite Noise Cost: the Support Bound, Swap, Displacement Couplings and Lower Semicontinuity of the Noise Cost
lemmalem:noise-cost-couplings-hilbert-2026aAnalysisProbabilityBasic properties of couplings of finite noise cost: the quadratic cost is bounded by a multiple of the noise cost, the class is stable under swapping the marginals, couplings induced by a map with finite noise displacement belong to it, and the noise cost is lower semicontinuous…Couplings of Finite Noise Cost and Their Noise Cost
definitiondef:noise-cost-coupling-hilbert-2026aAnalysisProbabilityA coupling of two Borel probability measures on the Hilbert space has finite noise cost when almost every displacement lies in the noise space and the mean squared noise norm of the displacement is finite; that mean is its noise cost. Two measures are noise-connected when they ad…Probability Measures on a Hilbert Space Transported in the Noise Norm: Standing Notation
settingset:noise-wasserstein-hilbert-2026aAnalysisProbabilityStanding notation for transport of Borel probability measures on a Hilbert space with an orthonormal basis measured in the noise norm of a fixed weight sequence: the noise weights, the noise space, square-integrable noise-valued fields, and a fixed reference measure.The Noise Space is a Real Hilbert Space: Orthonormal Basis, Continuous Embedding, Partial Sums, Closed Balls and Borel Measurability
lemmalem:noise-space-hilbert-2026aAnalysisProbabilityThe noise space of a bounded positive weight sequence is a real Hilbert space with orthonormal basis (a_k^{1/2} e_k), continuously embedded in the ambient space; its norm is the supremum of continuous partial sums, its closed balls are closed in the ambient space, and it and its…The Noise Space of a Weight Sequence on a Hilbert Space with an Orthonormal Basis
definitiondef:noise-space-hilbert-2026aAnalysisProbabilityFor a bounded positive weight sequence a on a Hilbert space with a fixed orthonormal basis, the noise space consists of the vectors whose coordinates satisfy sum x_k^2/a_k < infinity, with the inner product sum x_k y_k/a_k.Partial Derivatives along an Orthonormal Basis of a Function Differentiable on a Hilbert Space
definitiondef:partial-derivatives-basis-hilbert-2026aAnalysisDefines the k-th partial derivative of a function differentiable on a Hilbert space with an orthonormal basis as the k-th coordinate of its gradient.Bounded Continuously Differentiable Functions with Bounded Partial Derivatives on Euclidean Space
definitiondef:bounded-c1-functions-euclidean-2026aAnalysisDefines the bounded continuously differentiable functions on Euclidean space whose partial derivatives are bounded.Bounded Cylindrical Functions: Linear Structure, the Gradient and the Partial Derivatives, Bounds and Integrability, and Density in the Square-Integrable Functions
lemmalem:cylindrical-functions-hilbert-2026aAnalysisBounded C^1 cylindrical functions form a vector space containing the constants; each is differentiable with gradient given by its representation, so its partial derivatives are the Euclidean ones on the first n coordinates and vanish beyond; they are bounded and Borel with bounde…Bounded Cylindrical Functions on a Hilbert Space with an Orthonormal Basis
definitiondef:cylindrical-functions-hilbert-2026aAnalysisDefines bounded C^1 cylindrical functions on a Hilbert space with an orthonormal basis: functions of the first n coordinates through a bounded C^1 function with bounded derivatives, together with their representations.Weighted Square-Summable Sequence Spaces are Real Hilbert Spaces: the Standard Orthonormal Basis and the Embedding of a Hilbert Space under Bounded Weights
lemmalem:weighted-sequence-space-2026aAnalysisA weighted square-summable sequence space is a real Hilbert space with the rescaled unit sequences as orthonormal basis; under bounded weights the coordinate map embeds a Hilbert space with orthonormal basis continuously and injectively into it.- For positive weights, defines the space of real sequences whose squares are summable against the weights, with termwise operations and the weighted inner product.
Wasserstein Convergence on a Hilbert Space: Weak Convergence, Integrals of Continuous Functions of Quadratic Growth, Convergence from Weak Convergence with Uniformly Integrable Second Moments, and Compactness
lemmalem:wasserstein-convergence-hilbert-2026aAnalysisProbabilityWasserstein convergence on a Hilbert space implies weak convergence and convergence of integrals of continuous functions of quadratic growth; conversely weak convergence with uniformly integrable second moments implies Wasserstein convergence, which gives a compactness criterion.The Wasserstein Distance on a Hilbert Space as the Increasing Limit of the Euclidean Wasserstein Distances of the Coordinate Projections
lemmalem:wasserstein-projections-hilbert-2026aAnalysisProbabilityThe Wasserstein distance on a Hilbert space is the increasing limit of the Euclidean Wasserstein distances between the laws of the first n coordinates, and projecting onto the first n coordinates costs at most the tail second moment.The Quadratic Wasserstein Distance is a Metric on the Probability Measures with Finite Second Moment on a Hilbert Space
theoremthm:wasserstein-metric-hilbert-2026aAnalysisProbabilityThe quadratic Wasserstein distance is a metric on the Borel probability measures with finite second moment on a Hilbert space.Existence of an Optimal Coupling of Two Borel Probability Measures with Finite Second Moment on a Hilbert Space
theoremthm:optimal-coupling-exists-hilbert-2026aAnalysisProbabilityThe infimum defining the quadratic Wasserstein distance on a Hilbert space is attained by some coupling.The Quadratic Wasserstein Distance on a Hilbert Space
definitiondef:wasserstein-distance-hilbert-2026aAnalysisProbabilityDefines the quadratic Wasserstein distance between Borel probability measures with finite second moment on a Hilbert space.