Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.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.Pairings into a Product, the Graph of a Measurable Map, and Couplings Concentrated on a Graph
lemmalem:coupling-graph-pushforward-measurable-2026aProbabilityPairings of measurable maps are measurable into a product, the graph of a measurable map into a separable metric space is measurable, and a coupling concentrated on such a graph is the push-forward of its first marginal by the map.Conditioning in Two Steps: Composing a Conditional Kernel Given a Map with a Conditional Kernel Given a Function of It
lemmalem:conditional-kernel-composition-2026aProbabilityConditioning in two steps: averaging a conditional kernel given a map against a conditional kernel of that map's law given a function of it yields a conditional kernel given the composite.The Product of Two Probability Kernels is a Probability Kernel
lemmalem:product-probability-kernels-2026aProbabilityGiven two probability kernels with a common index space, taking the product measure index by index gives a probability kernel into the product space.The Conditional Kernel of a Probability Measure Given a Measurable Map
definitiondef:conditional-kernel-given-map-2026aProbabilityA conditional kernel of a probability measure given a measurable map is a probability kernel, indexed by the points of the target, whose average against the image measure over any target set reproduces the measure restricted to the preimage of that set.Talagrand's Inequality in the Noise Norm for a Diagonal Gaussian Reference Measure on a Hilbert Space
theoremthm:noise-talagrand-diagonal-gaussian-hilbert-2026aAnalysisProbabilityWhen the reference measure is a diagonal Gaussian whose variances are dominated by a constant multiple of the noise weights, every probability measure of finite relative entropy is noise-connected to it, and its squared noise Wasserstein distance to it is at most twice that const…The Conditional Law of the Head Given the Tail for a Measure with a Density Relative to a Diagonal Gaussian Measure on a Hilbert Space
lemmalem:diagonal-gaussian-fibre-conditional-hilbert-2026aProbabilityFor a probability measure with a density with respect to a diagonal Gaussian measure on a Hilbert space, the conditional law of the first n coordinates given the tail is, for almost every tail, the n-dimensional diagonal Gaussian reweighted by the density along the fibre and norm…Replacing the Tail of a Probability Measure on a Hilbert Space by an Independent Diagonal Gaussian Tail: Same Head and Convergence in the Quadratic Wasserstein Distance
lemmalem:gaussian-tail-approximation-hilbert-2026aProbabilityKeeping the first n coordinates of a measure with finite second moment and replacing its tail by an independent diagonal Gaussian tail gives measures with the same first n coordinates that converge to the original measure in the quadratic Wasserstein distance.