Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Gaussian-Tail Extensions: the Gaussian Reference Measure, Marginals, Densities, Relative Entropy, Relative Score and the Noise Wasserstein Distance
lemmalem:gaussian-tail-extension-hilbert-2026aProbabilityThe Gaussian reference measure is the Gaussian-tail extension of its rescaled head; extensions keep the head law, carry densities, relative entropy and relative score over from the head, and are no farther apart in the noise Wasserstein distance than their heads are in the Euclid…The Gaussian-Tail Extension of a Probability Measure on the Rescaled Head
definitiondef:gaussian-tail-extension-hilbert-2026aProbabilityThe Gaussian-tail extension at level n of a probability measure on R^n is the law on the Hilbert space whose rescaled head has that law and whose tail is an independent copy of the tail of the Gaussian reference measure.A Diagonal Gaussian Reference Measure on the Noise Wasserstein Space, Rescaled Heads and Gaussian Tails: Standing Notation
settingset:noise-gaussian-reference-hilbert-2026aProbabilityStanding notation for the noise Wasserstein space with a diagonal Gaussian reference measure: relative entropy and relative score with respect to it, the rescaled head maps and their lifts, the rescaled head variances, and the Gaussian tails with the synthesis map that joins a he…Relative Entropy over a Finite Partition: the Chain Rule, Images of the Pieces, Refinement and Approximation by Partition Entropies
lemmalem:relative-entropy-finite-partitions-measurable-2026aProbabilityFor a finite measurable partition, the relative entropy splits into the entropy of the cell masses plus the average entropy of the conditioned pieces; images of the pieces can only lose entropy; refining a partition can only increase the entropy of the cell masses; and suitable p…Relative Entropy of the Image under a Bimeasurable Bijection that Moves the Reference Measure by a Positive Density
lemmalem:relative-entropy-bijection-density-measurable-2026aProbabilityIf a bimeasurable bijection T carries the reference measure to a measure with a positive density g, then T carries a density f of a measure to the density (f∘T^{-1})g, and the relative entropy changes by the integral of log g∘T.Noise Gradients of Bounded Cylindrical Functions Are Dense in the Noise Tangent Space
lemmalem:c2-cylindrical-noise-gradients-dense-hilbert-2026aAnalysisProbabilityEvery bounded C^2 cylindrical function is a bounded C^1 cylindrical function, and for every Borel probability measure the noise gradients of bounded C^2 cylindrical functions approximate every element of the noise tangent space.Gaussian Smoothing of a Bounded Borel Function on Euclidean Space: the Two Forms, Derivatives through the Kernel and through the Function, and Pointwise Convergence
lemmalem:gaussian-smoothing-bounded-function-euclidean-2026aAnalysisThe convolution of a bounded Borel function with a Gaussian kernel is bounded by the same constant, continuously differentiable with derivatives computed through the kernel, commutes with differentiation when the function is bounded C^1, and converges to the function at its point…Bounded Cylindrical Functions on a Hilbert Space with an Orthonormal Basis
definitiondef:bounded-c2-cylindrical-functions-hilbert-2026aAnalysisDefines the bounded C^2 cylindrical functions on a Hilbert space with a fixed orthonormal basis: functions of finitely many coordinates given by a bounded C^2 function with bounded first and second derivatives.Bounded Twice Continuously Differentiable Functions with Bounded First and Second Partial Derivatives on Euclidean Space
definitiondef:bounded-c2-functions-euclidean-2026aAnalysisDefines the set of twice continuously differentiable real functions on Euclidean space that are bounded together with all their first and second partial derivatives.The Entropy Domain of a Diagonal Gaussian Reference Measure Has the Noise Map Property
corollarycor:noise-map-property-entropy-diagonal-gaussian-hilbert-2026aAnalysisProbabilityWhen the reference measure is a diagonal Gaussian measure whose variances are dominated by a multiple of the noise weights, the measures of finite relative entropy form a set with the noise map property.Tangency of Noise-Optimal Displacements out of a Measure with a Density Relative to a Diagonal Gaussian Measure, and the Noise Map Property
theoremthm:noise-tangency-absolutely-continuous-hilbert-2026aAnalysisProbabilityOut of a measure with a density relative to a diagonal Gaussian measure, every noise-optimal displacement lies in the noise tangent space; hence the set of such measures has the noise map property.Strong Convergence of Noise Displacement Fields from Weak Convergence of Their Graph Couplings and an Upper Bound on Their Norms
lemmalem:graph-coupling-strong-convergence-hilbert-2026aAnalysisProbabilityIf the graph couplings of noise displacement fields converge weakly to the graph coupling of a limit field, and their norms are eventually at most the norm of the limit plus any margin, then the fields converge strongly among the square-integrable noise fields.Measures Whose Heads Agree with a Fixed Measure and Whose Tails Vanish Converge in the Quadratic Wasserstein Distance
lemmalem:head-matched-w2-convergence-hilbert-2026aAnalysisProbabilityIf the n-th measure of a sequence has the same law of the first n coordinates as a fixed measure and its tail second moments tend to zero, the sequence converges to the fixed measure in the quadratic Wasserstein distance.Lifting Euclidean Tangent Fields of the Rescaled Head to Noise Tangent Fields on a Hilbert Space
lemmalem:noise-head-lift-tangent-hilbert-2026aAnalysisProbabilityRescaling the first n coordinates by the noise weights lifts Euclidean vector fields on the head to noise fields on the Hilbert space. The lift is a linear isometry sending gradients of test functions to noise gradients of cylindrical functions, hence Euclidean tangent fields int…Noise-Optimal Maps out of the Entropy Domain of a Diagonal Gaussian Reference Measure
corollarycor:noise-brenier-entropy-diagonal-gaussian-hilbert-2026aProbabilityWith a diagonal Gaussian reference measure dominated by the noise, every measure of finite relative entropy is noise-connected to the reference and is uniquely noise-mapped to every noise-connected measure.Brenier's Theorem in the Noise Norm: Noise-Optimal Couplings out of a Measure with a Density Relative to a Diagonal Gaussian Measure are Induced by a Unique Map
theoremthm:noise-brenier-hilbert-2026aProbabilityIf the source measure has a density relative to some diagonal Gaussian measure, every noise-optimal coupling is induced by a noise-optimal map, and the optimal coupling is unique.Head Maps of a Noise-Optimal Coupling: the Head of the Target is a Function of the Source
lemmalem:noise-head-maps-hilbert-2026aProbabilityFor a noise-optimal coupling out of a measure with a density relative to a diagonal Gaussian measure, the first n coordinates of the target are almost surely a Borel function of the source.The Head Given the Tail is Absolutely Continuous for a Measure with a Density Relative to a Diagonal Gaussian Measure
corollarycor:diagonal-gaussian-head-conditional-ac-hilbert-2026aProbabilityFor a measure with a density relative to a diagonal Gaussian measure, the conditional law of the first n coordinates given the tail is absolutely continuous for almost every tail.Fibrewise Cyclical Monotonicity of a Noise-Optimal Coupling: Given the Tail, the Heads are Cyclically Monotone
lemmalem:noise-fibre-cyclically-monotone-hilbert-2026aProbabilityFor a noise-optimal coupling disintegrated along the tail of the source, almost every fibre law of the pair (head of the source, rescaled head of the target) has cyclically monotone support.A Coupling on Euclidean Space with an Absolutely Continuous First Marginal and Cyclically Monotone Support is Induced by a Map
lemmalem:cyclically-monotone-coupling-map-euclidean-2026aProbabilityA probability measure on a doubled Euclidean space whose first marginal is absolutely continuous and whose support is cyclically monotone is concentrated on the graph of a Borel map, with no optimality or moment assumption.