Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Gaussian Entropy Pair Has Regular Penalised Maxima
lemmalem:noise-gaussian-entropy-pair-regular-maxima-hilbert-2026aAnalysisProbabilityEvery local maximum of a noise intrinsic test function minus a positive multiple of the Gaussian entropy penalty has finite weighted Fisher information.The Gaussian Entropy Pair Has Closed Score Along Noise Couplings
lemmalem:noise-gaussian-entropy-pair-closed-score-hilbert-2026aAnalysisProbabilityAlong couplings of vanishing noise cost, measures with uniformly bounded scores converge to a measure that again has finite weighted Fisher information, and the scores converge weakly along the couplings.The Gaussian Entropy Pair is Noise-Closed, and Its Penalty Bounds the Squared Noise Wasserstein Distance to the Reference Measure
lemmalem:noise-gaussian-entropy-pair-closed-hilbert-2026aAnalysisProbabilityThe Gaussian entropy pair has closed and bounded penalty sublevel sets in the noise Wasserstein space, and by Talagrand's inequality the squared distance to the reference measure is at most 2 kappa over beta times the penalty.The Gaussian Entropy Pair is a Noise Penalty Pair, with Nonnegative Penalty and Dense Score Domain
lemmalem:noise-gaussian-entropy-penalty-pair-hilbert-2026aAnalysisProbabilityThe Gaussian entropy pair is a noise penalty pair: its penalty is nonnegative and measures of finite weighted Fisher information are dense among measures of finite relative entropy in the noise Wasserstein distance.A Bound on the Noise Ornstein-Uhlenbeck Functional by Noise Gradients Gives Finite Weighted Fisher Information
lemmalem:ou-functional-fisher-bound-hilbert-2026aAnalysisProbabilityIf the noise Ornstein-Uhlenbeck functional of a measure is bounded by R times the noise-gradient norm on bounded C^2 cylindrical functions, then the measure has a relative score and weighted Fisher information at most R squared.The Gaussian Entropy Pair on the Noise Wasserstein Space: Relative Entropy and the Noise Score Field
definitiondef:noise-gaussian-entropy-pair-hilbert-2026aAnalysisProbabilityDefines the Gaussian entropy pair on the noise Wasserstein space: the penalty is beta times relative entropy with respect to the diagonal Gaussian reference measure, and the score is beta times the noise score field on measures of finite weighted Fisher information.The Conditioned Probability Measure Given a Set of Positive Measure
definitiondef:conditioned-probability-measure-2026aProbabilityThe probability measure conditioned on a measurable set of positive mass is its restriction to that set, normalised by the mass of the set.The Noise Ornstein-Uhlenbeck Functional of a Probability Measure at a Bounded Function of Finitely Many Coordinates
definitiondef:noise-ou-functional-hilbert-2026aProbabilityFor a probability measure with finite second moment and a bounded C^2 function g of the first n coordinates, the noise Ornstein-Uhlenbeck functional is the a_k-weighted sum of the integrals of x_k times the k-th partial derivative of g divided by c_k, minus the k-th pure second p…The Partition Entropy of a Probability Measure Relative to Another over a Finite Measurable Partition
definitiondef:partition-entropy-measurable-2026aProbabilityThe partition entropy of one probability measure relative to another over a finite measurable partition is the relative entropy of their vectors of cell masses, defined when every cell charged by the first measure is charged by the second.Finite Measurable Partitions and Their Refinements
definitiondef:finite-measurable-partition-2026aProbabilityA finite measurable partition is a finite family of pairwise disjoint measurable sets covering the space, empty cells allowed; one partition refines another if each of its cells lies in a cell of the other.Lifted Optimal Maps between Rescaled Heads Converge Strongly to the Noise-Optimal Displacement
lemmalem:head-approximation-noise-optimal-displacement-hilbert-2026aProbabilityFor a uniquely noise-mapped pair, the optimal Euclidean maps between the rescaled heads, lifted back to the Hilbert space, have cost at most the squared noise Wasserstein distance and converge strongly to the displacement of the noise-optimal map.Tail Replacement in the Noise Wasserstein Distance: a Measure of Finite Relative Entropy is Approximated by the Gaussian-Tail Extensions of Its Rescaled Heads
lemmalem:tail-replacement-noise-wasserstein-hilbert-2026aProbabilityReplacing the tail of a measure of finite relative entropy by an independent Gaussian tail costs, in squared noise Wasserstein distance, at most 2 kappa times the relative entropy lost by passing to the rescaled head; hence the Gaussian-tail extensions of the rescaled heads conve…The Noise Score Field of a Measure of Finite Weighted Fisher Information: Existence, Norm, Pairing with Noise Gradients, Head Approximation and Tangency
lemmalem:noise-score-field-hilbert-2026aProbabilityA measure with a relative score of finite weighted Fisher information carries a unique square-integrable noise field whose coordinates are the weighted score components; its squared norm is the weighted Fisher information, its pairing with a noise gradient is the Ornstein-Uhlenbe…The Relative Score of the Rescaled Head: Projections of the Score, the Ornstein-Uhlenbeck Functional of the Head, and the Converse under Bounded Head Fisher Information
lemmalem:relative-score-rescaled-head-hilbert-2026aProbabilityThe rescaled head of a measure with a relative score has finite Fisher information relative to the rescaled Gaussian, its score components are the rescaled projections of the score components, and its Fisher information is the weighted head Fisher information; the noise Ornstein-…Relative Entropy along a Noise-Gradient Perturbation of the Identity: the Formula, the Second-Order Expansion and the First Variation
lemmalem:relative-entropy-noise-gradient-perturbation-hilbert-2026aProbabilityPushing a measure of finite relative entropy with respect to the diagonal Gaussian measure forward by the identity plus a small multiple of the noise gradient of a bounded C^2 cylindrical function keeps the relative entropy finite, changes it by an explicit integral, and differen…Moving the Rescaled Head of the Diagonal Gaussian Measure by a Diffeomorphism: the Image Has an Explicit Positive Density Depending on the Head Only
lemmalem:diagonal-gaussian-head-map-density-hilbert-2026aProbabilityApplying a diffeomorphism F with symmetric positive definite Jacobian to the rescaled head, and leaving the tail fixed, is a bijection of the Hilbert space; it carries the diagonal Gaussian measure to a measure whose density with respect to it is an explicit positive function of…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…