Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.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…