Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Measures Noise-Connected to the Reference Measure
definitiondef:noise-wasserstein-space-hilbert-2026aAnalysisProbabilityThe set of Borel probability measures on a Hilbert space that are noise-connected to the fixed reference measure.- For a noise-connected ordered pair of Borel probability measures on a Hilbert space, a coupling of finite noise cost is noise-optimal if its noise cost equals the square of the noise Wasserstein distance.
Squared Noise Wasserstein Distances, Their Convergent Series and Linear Combinations are Noise Intrinsic Test Functions
lemmalem:noise-w2-squared-test-function-hilbert-2026aAnalysisProbabilityOn a set with the noise map property, the squared noise Wasserstein distance to a fixed measure and convergent weighted series of squared distances to measures at bounded distance from the reference measure are noise intrinsic test functions, with gradients given by optimal displ…Noise Intrinsic Test Functions on the Noise Wasserstein Space
definitiondef:noise-intrinsic-test-function-hilbert-2026aAnalysisProbabilityA real function on the noise Wasserstein space is a noise intrinsic test function on a set of measures if it is continuous, differentiable along noise couplings at each point of the set with gradient in the noise tangent space, and its gradient is continuous along couplings of va…The Noise-Optimal Map: Transport Cost, Stability Along Nearly Optimal Couplings and Stability Under Perturbation of the Source
theoremthm:noise-optimal-map-stability-hilbert-2026aAnalysisProbabilityThe displacement of a noise-optimal map has squared norm equal to the squared noise Wasserstein distance; for a uniquely noise-mapped pair, couplings of nearly optimal noise cost concentrate on the graph of the map in mean square; and the optimal displacements to a fixed target a…Noise-Optimal Maps and Uniquely Noise-Mapped Pairs
definitiondef:noise-optimal-map-hilbert-2026aAnalysisProbabilityDefines a noise-optimal transport map between two measures (a Borel map pushing one to the other whose displacement lies in the noise space with finite noise cost and whose induced coupling is noise-optimal), uniquely noise-mapped pairs, and the noise map property of a set of mea…Strong and Weak Convergence of Noise Fields Along Couplings of Vanishing Noise Cost
definitiondef:noise-field-convergence-hilbert-2026aAnalysisProbabilityDefines sequences of couplings of vanishing noise cost, and strong and weak convergence of noise fields along them, via the discrepancy and the cross pairing.Completeness of the Quadratic Wasserstein Space and of the Noise Wasserstein Space over a Hilbert Space
theoremthm:noise-wasserstein-complete-hilbert-2026aAnalysisProbabilityThe quadratic Wasserstein space over the Hilbert space is complete, and so is the noise Wasserstein space based at the reference measure.Differentiability of a Function on the Noise-Connected Measures Along Noise Couplings, and Its Gradient
definitiondef:noise-differentiable-along-couplings-hilbert-2026aAnalysisProbabilityA real function on the measures noise-connected to the reference measure is differentiable along noise couplings at a measure if its increments are approximated, to first order in the square root of the noise cost, by the noise displacement pairing with a noise field; that field…Cauchy Sequences in the Quadratic Wasserstein Space and Weakly Convergent Sequences on a Hilbert Space are Tight
lemmalem:w2-cauchy-tight-hilbert-2026aAnalysisProbabilityEvery Cauchy sequence for the quadratic Wasserstein distance of probability measures with finite second moment on a separable Hilbert space is a tight sequence of measures.Noise Displacement and Cross Pairings Along Couplings: Bounds, Linearity, Displacement Couplings, Polarisation and a Vanishing Criterion
lemmalem:noise-displacement-pairing-hilbert-2026aAnalysisProbabilityAlong a coupling of finite noise cost the displacement is a square-integrable noise field whose squared norm is the noise cost; pairing it with a noise field gives a bounded linear functional, computed explicitly along displacement couplings. Also: the cross pairing of two noise…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.