Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Talagrand's Inequality for a Diagonal Gaussian Measure on Euclidean Space in the Cameron-Martin Cost
lemmalem:talagrand-diagonal-gaussian-euclidean-2026aAnalysisProbabilityA probability measure with finite relative entropy with respect to a diagonal Gaussian measure on Euclidean space is the image of the Gaussian under a Borel map whose transport cost, with each coordinate weighted by the inverse of its variance, is at most twice the relative entro…Head and Tail of a Diagonal Gaussian Measure on a Hilbert Space are Independent
lemmalem:diagonal-gaussian-head-tail-hilbert-2026aProbabilityUnder a diagonal Gaussian measure on a Hilbert space, the first n coordinates and the remaining tail are independent: the joint law of head and tail is the product of the n-dimensional diagonal Gaussian with the law of the tail, and the measure is recovered from this product by a…Conditional Kernels of a Borel Probability Measure on a Polish Space Given a Borel Map: Existence, Uniqueness and Concentration on the Fibres
corollarycor:conditional-kernel-given-map-polish-2026aAnalysisProbabilityGiven a Borel map from a complete separable metric space into a separable metric space, every Borel probability measure has a conditional kernel given the map, unique up to a null set of the image measure; almost every conditional measure is carried by its fibre, and integrals ag…Disintegration of a Probability Measure on a Product with a Polish Factor: Existence and Almost-Everywhere Uniqueness of the Conditional Kernel
theoremthm:disintegration-polish-2026aAnalysisProbabilityA probability measure on the product of a measurable space and a complete separable metric space is the composite of its first marginal with a probability kernel, and this kernel is unique up to a null set of the marginal.Integration Against a Probability Kernel: Measurable Sections, the Composite Measure on the Product and the Iterated Integral
lemmalem:probability-kernel-integration-2026aAnalysisProbabilityA probability measure and a probability kernel define a unique probability measure on the product sigma-algebra, against which nonnegative functions are integrated by first integrating against the kernel and then against the measure.- A probability kernel assigns to each point of one measurable space a probability measure on another, measurably in the point.
Extension of a Finite Premeasure from an Algebra of Sets to the Generated Sigma-Algebra
theoremthm:premeasure-extension-2026aAnalysisProbabilityA finite, countably additive set function on an algebra of subsets extends to a measure on the generated sigma-algebra, and the extension is unique.The Borel Sigma-Algebra of a Product of Two Separable Metric Spaces is the Product Sigma-Algebra
lemmalem:borel-product-separable-metric-2026aAnalysisProbabilityFor two separable metric spaces, the Borel sets of the product metric space are exactly the sets of the product sigma-algebra of the two Borel sigma-algebras.Perron's Method on the Noise Wasserstein Space: Existence of a Viscosity Solution of a First-Order Equation Between a Subsolution and a Supersolution
theoremthm:noise-perron-existence-hilbert-2026bAnalysisProbabilityPDEFor a noise-closed noise penalty pair with regular penalised maxima whose penalty domain has the noise map property, and any first-order equation operator, the pointwise supremum of all viscosity subsolutions lying between a given subsolution and a given supersolution above it, b…Well-Posedness of the Hamilton-Jacobi Equation with Penalty Drift on the Noise Wasserstein Space: Comparison, Existence and Uniqueness of a Bounded Viscosity Solution
theoremthm:noise-penalty-drift-well-posed-hilbert-2026bAnalysisProbabilityPDEFor a displacement convex, noise-closed noise penalty pair with closed score and regular penalised maxima whose penalty domain has the noise map property and whose penalty controls the squared distance to the reference measure, and for a bounded uniformly continuous running cost…Constant Viscosity Subsolutions and Supersolutions of the Hamilton-Jacobi Equation with Penalty Drift on the Noise Wasserstein Space
lemmalem:noise-constant-sub-supersolutions-hilbert-2026bAnalysisProbabilityPDEFor a noise-closed noise penalty 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…The Hamilton-Jacobi Operator with Penalty Drift on the Noise Wasserstein Space Satisfies the Hypotheses of the First-Order Comparison Principle for a Displacement Convex Noise Penalty Pair
lemmalem:noise-penalty-drift-hypotheses-hilbert-2026bAnalysisProbabilityPDEFor a displacement convex noise penalty pair with lower semicontinuous penalty whose squared noise Wasserstein distance to the reference measure is controlled by the penalty, control cost at most one and a bounded uniformly continuous running cost, the penalty-drift Hamilton-Jaco…A Comparison Principle for First-Order Equations on the Noise Wasserstein Space Relative to a Noise-Closed Penalty Pair
theoremthm:noise-comparison-first-order-hilbert-2026bAnalysisProbabilityPDEComparison without compactness on the noise Wasserstein space: for a noise-closed penalty pair with closed score whose domain has the noise map property, and a first-order operator that is locally strictly proper, shift-coercive, shift-semicontinuous, satisfies the structure cond…The Bump Construction on the Noise Wasserstein Space: the Local Maximum of a Viscosity Subsolution and a Penalised Noise Intrinsic Test Function
lemmalem:noise-perron-bump-hilbert-2026bAnalysisProbabilityPDEInside a noise Wasserstein ball, replace a viscosity subsolution v by the maximum of v and a test function minus a multiple of the penalty, which stays below v near the edge of the ball. If the test function satisfies the shifted subsolution inequality wherever it wins, the resul…Exact Inequalities at a Touching Point of a Penalised Viscosity Subsolution or Supersolution on the Noise Wasserstein Space
lemmalem:noise-penalised-exact-jets-hilbert-2026bAnalysisProbabilityPDEFor a noise-closed penalty pair with closed score and a first-order operator satisfying shift-coercivity and shift-semicontinuity, a point where a noise intrinsic test function touches the delta-envelope of a penalised viscosity subsolution (or supersolution) lies in the score do…The Pointwise Supremum of a Uniformly Subordinate Family of Viscosity Subsolutions on the Noise Wasserstein Space is a Viscosity Subsolution
lemmalem:noise-sup-of-subsolutions-hilbert-2026bAnalysisProbabilityPDEFor a noise-closed noise penalty pair whose penalty domain has the noise map property, the pointwise supremum of a nonempty family of viscosity subsolutions of a first-order equation that is uniformly subordinate from above is again a viscosity subsolution.Bounds, Monotonicity and Borwein-Preiss Perturbed Maximisers of the Doubled Difference in the Noise Wasserstein Distance for a Noise-Closed Penalty Pair
lemmalem:noise-doubling-perturbed-maximiser-hilbert-2026bAnalysisProbabilityPDEFor a noise-closed penalty pair and bounded u, v, the difference of their delta-envelopes doubled with the squared noise Wasserstein distance has a finite supremum, monotone in the weight and in the doubling strength with slack, and a Borwein-Preiss perturbed maximiser: a near-ma…The First-Order Condition at a Penalised Extremum of a Noise Intrinsic Test Function on the Noise Wasserstein Space
lemmalem:noise-penalised-extremum-hilbert-2026bAnalysisProbabilityAt a point of the score domain at which a noise intrinsic test function minus a positive multiple of the penalty has a local maximum on the penalty domain, the gradient along noise couplings equals that multiple of the score; at a local minimum of the test function plus the penal…A Toolkit for Penalised Comparison on the Noise Wasserstein Space: Constant Test Functions and Linear Combinations of Test Functions, the Identity as a Unique Noise-Optimal Map, and Discrepancies Along the Push-Forward Under (id, id) and Along Glued Couplings
lemmalem:noise-penalty-toolkit-hilbert-2026bAnalysisProbabilityConstant functions are noise intrinsic test functions with zero gradient, and real linear combinations of noise intrinsic test functions are again such functions, with the corresponding linear combination of gradients; the identity is a noise-optimal map from a measure to itself…Basic Properties of the Delta-Envelopes on the Noise Wasserstein Space, and the Envelopes of Bounded Functions for a Noise-Closed Penalty Pair
lemmalem:noise-delta-envelopes-hilbert-2026bAnalysisProbabilityThe delta-envelopes relative to a noise penalty pair are semicontinuous and placed on the correct side of the penalised function, are exchanged by negation, are exact for continuous functions and a lower semicontinuous penalty, and inherit bounds by a smaller multiple of the pena…