Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.The Weighted Fisher Information Relative to a Diagonal Gaussian Measure on Euclidean Space
definitiondef:weighted-fisher-information-euclidean-2026aProbabilityFor a measure on Euclidean space with finite Fisher information relative to a diagonal Gaussian and positive weights, defines the weighted Fisher information as the integral of the weighted sum of squares of the components of the relative score.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.Weight Sequences and the Weighted Fisher Information Relative to a Diagonal Gaussian Measure on a Hilbert Space
definitiondef:weighted-fisher-information-hilbert-2026aProbabilityDefines weight sequences (bounded sequences of positive numbers) and the Fisher information relative to a diagonal Gaussian with given weights: the weighted sum of the squared L^2 norms of the score components, when it converges.Relative Scores of the Finite-Dimensional Projections on a Hilbert Space: Orthogonal Projections of the Score, and the Weighted Fisher Information as the Limit of Its Cutoffs
lemmalem:relative-score-projections-hilbert-2026aProbabilityFor a measure on a Hilbert space with a relative score, the finite-dimensional projections have finite Fisher information and their scores are the orthogonal projections of the score components onto functions of the first n coordinates; the weighted cutoff Fisher informations inc…Finite Fisher Information Relative to a Diagonal Gaussian Measure on Euclidean Space as Componentwise Integration by Parts against Bounded Functions
lemmalem:relative-score-componentwise-euclidean-2026aProbabilityOn Euclidean space, finite Fisher information relative to a diagonal Gaussian, defined through the tangent space, is equivalent to componentwise Gaussian integration by parts against bounded C^1 functions; the components are then unique and equal to those of the relative score, a…The Relative Score on a Hilbert Space: the Gaussian Measure Has Score Zero, and the Score as a Square-Integrable Field in the Weighted Sequence Space
lemmalem:relative-score-basic-hilbert-2026aProbabilityThe diagonal Gaussian measure has relative score zero and zero weighted Fisher information; and a measure with finite weighted Fisher information has a unique score field in the square-integrable maps into the weighted sequence space, whose squared norm is the Fisher information.The Relative Score with Respect to a Diagonal Gaussian Measure on a Hilbert Space
definitiondef:relative-score-diagonal-gaussian-hilbert-2026aProbabilityA probability measure with finite second moment on a Hilbert space has a relative score with respect to a diagonal Gaussian when, for each coordinate, Gaussian integration by parts against bounded C^1 cylindrical functions is represented by a square-integrable function; the score…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.
The Space of Square-Integrable Hilbert-Valued Maps is a Real Hilbert Space: Coordinates and Synthesis
lemmalem:square-integrable-maps-hilbert-valued-2026aProbabilityThe space of square-integrable Hilbert-valued maps is a real Hilbert space; its inner product is the sum of the scalar L^2 inner products of the coordinates, and every square-summable sequence of scalar classes is the coordinate sequence of exactly one element.