Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Changing the Variances of a Diagonal Gaussian Reference Measure: Equal Domains, the Shift of the Relative Entropy and the Shift of the Relative Score
lemmalem:change-of-variances-diagonal-gaussian-euclidean-2026aAnalysisProbabilityTwo diagonal Gaussian reference measures give the same measures of finite relative entropy and of finite relative Fisher information; the relative entropies differ by half the integral of the difference of the weighted squares plus a constant, and the relative scores differ by th…Gaussian Integration by Parts Relative to a Diagonal Gaussian Measure for Functions with a Bounded Hessian
lemmalem:gaussian-integration-by-parts-diagonal-euclidean-2026aAnalysisProbabilityFor a measure of finite Fisher information relative to a diagonal Gaussian, the pairing of its relative score with the gradient of a function with bounded Hessian equals minus the integral of the Ornstein-Uhlenbeck generator applied to the function.Well-Posedness of the Lifted Ornstein-Uhlenbeck Hamilton-Jacobi Equation Relative to a Diagonal Gaussian Measure: Comparison, Existence and Uniqueness of a Bounded Viscosity Solution
theoremthm:lifted-ou-hamilton-jacobi-well-posed-euclidean-2026aAnalysisProbabilityPDEFor a bounded, Wasserstein-uniformly continuous running cost and control cost theta in (0,1], the lifted Ornstein-Uhlenbeck Hamilton-Jacobi equation relative to a diagonal Gaussian satisfies comparison and has exactly one bounded viscosity solution on the finite-entropy measures,…A Comparison Principle for First-Order Equations on the Wasserstein Space Relative to a Wasserstein-Closed Penalty Pair
theoremthm:comparison-first-order-w2-closed-wasserstein-2026aAnalysisPDEComparison without compactness: for a Wasserstein-closed penalty pair with closed score whose domain has the map property, and a first-order operator (independent of the matrix argument) that is locally strictly proper, shift-coercive, shift-semicontinuous, satisfies the structur…Constant Viscosity Subsolutions and Supersolutions of the Hamilton-Jacobi Equation with Common Noise and Penalty Drift
lemmalem:constant-sub-supersolutions-penalty-drift-wasserstein-2026aAnalysisPDEFor a Wasserstein-closed pair with regular penalised maxima, a constant function has penalty-subordinate growth from both sides; it is a viscosity subsolution of the penalty-drift Hamilton-Jacobi equation when discount times the constant is at most the running cost on the score d…The Hamilton-Jacobi Operator with Common Noise and Penalty Drift Has Momentum-Continuous Shifts
lemmalem:penalty-drift-momentum-continuous-wasserstein-2026aAnalysisPDEThe delta-shifts of the Hamilton-Jacobi operator with common noise and penalty drift are Lipschitz in the vector field, with constant (2 theta + 1) R on data of score and field norms at most R; hence the operator has momentum-continuous shifts.Bounds, Monotonicity and Borwein-Preiss Perturbed Maximisers of the Wasserstein-Doubled Difference for a Wasserstein-Closed Penalty Pair
lemmalem:w2-doubling-perturbed-maximiser-wasserstein-2026aAnalysisPDEFor a Wasserstein-closed pair and bounded u, v, the Wasserstein-doubled difference of their delta-envelopes has a finite supremum, monotone in the weight and in the doubling strength with slack, and a Borwein-Preiss perturbed maximiser: a near-maximising pair, localised in a subl…Exact Inequalities at a Touching Point of a Penalised Viscosity Subsolution or Supersolution on the Wasserstein Space
lemmalem:penalised-exact-jets-wasserstein-2026aAnalysisPDEFor a Wasserstein-closed pair with closed score and an operator satisfying shift-coercivity and shift-semicontinuity, a point where an intrinsic test function touches the delta-envelope of a penalised viscosity subsolution (or supersolution) lies in the score domain, and the shif…A Convergent Series of Squared Wasserstein Distances to Measures of Bounded Second Moment is an Intrinsic Test Function
lemmalem:w2-squared-series-intrinsic-test-function-wasserstein-2026aAnalysisProbabilityA convergent positive series of squared Wasserstein distances to measures with uniformly bounded second moments defines an intrinsic test function on any set with the map property; its gradient is the corresponding series of displacement fields, bounded by twice the series of dis…The Gaussian Free-Energy Pair is Wasserstein-Closed
lemmalem:gaussian-free-energy-pair-w2-closed-euclidean-2026aAnalysisProbabilityThe Gaussian free-energy pair (relative entropy with respect to a diagonal Gaussian, with the relative score) is Wasserstein-closed, although it is not Wasserstein-coercive.Basic Properties of a Wasserstein-Closed Penalty Pair: Lower Bound, Lower Semicontinuity, Complete Sublevel Sets, Bounded Distances, and Coercive Pairs
lemmalem:w2-closed-penalty-pair-basic-wasserstein-2026aAnalysisProbabilityFor a Wasserstein-closed penalty pair the penalty is bounded below and lower semicontinuous, each sublevel set is a complete metric space on which squared Wasserstein distances are bounded by four times the moment bound, and every Wasserstein-coercive pair is Wasserstein-closed.The Lifted Ornstein-Uhlenbeck Hamilton-Jacobi Equation Relative to a Diagonal Gaussian Measure
equationeq:lifted-ou-hamilton-jacobi-euclidean-2026aAnalysisProbabilityPDEThe lifted Ornstein-Uhlenbeck Hamilton-Jacobi equation: the penalty-drift Hamilton-Jacobi equation of the Gaussian free-energy pair without common noise, lambda r + (theta/2)|q|^2 + a<relative score, q> = g, with viscosity solutions relative to the Gaussian free-energy pair.Equation Operators on the Wasserstein Space with Momentum-Continuous Shifts
definitiondef:momentum-continuous-shifts-wasserstein-2026aAnalysisPDEAn equation operator on the Wasserstein space has momentum-continuous shifts if, at each weight delta in (0,1) and each level R, its two delta-shifts are uniformly continuous in the vector-field argument over data bounded by R with score bounded by R.Wasserstein-Closed Penalty Pairs
definitiondef:w2-closed-penalty-pair-wasserstein-2026aAnalysisProbabilityA penalty pair is Wasserstein-closed if each sublevel set of its penalty is closed in the Wasserstein space (limits of sequences with penalty at most c stay in the domain with penalty at most c) and has bounded second moments. It weakens Wasserstein-coercivity, which asks for com…The Diagonal Gaussian Density on Euclidean Space and Its Notation
definitiondef:diagonal-gaussian-density-euclidean-2026aAnalysisProbabilityFor a vector of positive variances, fixes the scaling map x -> (x_i/c_i), the weighted square sum x_i^2/c_i, the log-normalizer, and the diagonal Gaussian density exp(-weighted square/2 - log-normalizer) on R^d.Completeness of the Quadratic Wasserstein Space over Euclidean Space
theoremthm:wasserstein-space-complete-euclidean-2026aAnalysisProbabilityThe space of probability measures on R^d with finite second moment, with the quadratic Wasserstein distance, is a complete metric space.The Gaussian Free-Energy Pair is Uniformly Displacement Convex, with Closed Score Along Couplings and Regular Penalised Maxima
lemmalem:gaussian-free-energy-pair-regularity-euclidean-2026aAnalysisProbabilityThe Gaussian free-energy pair is (a/c_max)-displacement convex, has closed score along couplings, and has regular penalised maxima.The Gaussian Free-Energy Pair is a Penalty Pair: Translations, the First Variation, Lower Semicontinuity, the Moment Bound and the Map Property
lemmalem:gaussian-free-energy-penalty-pair-euclidean-2026aAnalysisProbabilityThe Gaussian free-energy pair is a penalty pair: translations change the penalty by an explicit quadratic, so its translation Hessian is diagonal with entries a/c_i; its first variation along gradients of test functions is minus the temperature times the Ornstein-Uhlenbeck functi…The Gaussian Free-Energy Pair: Relative Entropy and Relative Score with Respect to a Diagonal Gaussian Measure
definitiondef:gaussian-free-energy-pair-euclidean-2026aAnalysisProbabilityThe Gaussian free-energy pair has as penalty the temperature times the relative entropy with respect to a diagonal Gaussian, on measures of finite second moment and finite relative entropy, and as score the temperature times the relative score, on those of finite relative Fisher…The Entropy Inequality for Nonnegative Functions, and Quadratic Moments Bounded by the Relative Entropy with Respect to a Diagonal Gaussian Measure
lemmalem:entropy-quadratic-moment-diagonal-gaussian-euclidean-2026aAnalysisProbabilityThe integral of a nonnegative function is at most the relative entropy plus the logarithm of its exponential moment under the reference measure; relative to a diagonal Gaussian this bounds diagonal quadratic moments, and the second moment, linearly by the relative entropy with ex…