Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Diagonal Gaussian Measures on a Hilbert Space
definitiondef:diagonal-gaussian-measure-hilbert-2026aProbabilityThe diagonal Gaussian measure with a variance sequence c is the unique Borel probability measure on the Hilbert space whose projections onto the first n coordinates are the diagonal Gaussian measures with the first n variances.The Diagonal Gaussian Random Series in a Hilbert Space: Almost Sure Convergence, Finite-Dimensional Projections, and the Unique Measure with Diagonal Gaussian Projections
lemmalem:diagonal-gaussian-random-series-hilbert-2026aProbabilityFor positive summable variances and independent standard normal coefficients, the random series of the scaled basis vectors converges almost surely to a random element of the Hilbert space whose finite-dimensional projections are diagonal Gaussian; exactly one Borel probability m…Kolmogorov's Maximal Inequality and the Convergence of Series of Independent Square-Integrable Random Variables
theoremthm:kolmogorov-independent-series-2026aProbabilityFor independent centred square-integrable random variables with summable variances, Kolmogorov's maximal inequality holds for the partial sums, the series converges almost surely, and its sum is square-integrable with the tail variances as mean-square error.Wasserstein Convergence on a Hilbert Space: Weak Convergence, Integrals of Continuous Functions of Quadratic Growth, Convergence from Weak Convergence with Uniformly Integrable Second Moments, and Compactness
lemmalem:wasserstein-convergence-hilbert-2026aAnalysisProbabilityWasserstein convergence on a Hilbert space implies weak convergence and convergence of integrals of continuous functions of quadratic growth; conversely weak convergence with uniformly integrable second moments implies Wasserstein convergence, which gives a compactness criterion.The Wasserstein Distance on a Hilbert Space as the Increasing Limit of the Euclidean Wasserstein Distances of the Coordinate Projections
lemmalem:wasserstein-projections-hilbert-2026aAnalysisProbabilityThe Wasserstein distance on a Hilbert space is the increasing limit of the Euclidean Wasserstein distances between the laws of the first n coordinates, and projecting onto the first n coordinates costs at most the tail second moment.The Quadratic Wasserstein Distance is a Metric on the Probability Measures with Finite Second Moment on a Hilbert Space
theoremthm:wasserstein-metric-hilbert-2026aAnalysisProbabilityThe quadratic Wasserstein distance is a metric on the Borel probability measures with finite second moment on a Hilbert space.Existence of an Optimal Coupling of Two Borel Probability Measures with Finite Second Moment on a Hilbert Space
theoremthm:optimal-coupling-exists-hilbert-2026aAnalysisProbabilityThe infimum defining the quadratic Wasserstein distance on a Hilbert space is attained by some coupling.The Quadratic Wasserstein Distance on a Hilbert Space
definitiondef:wasserstein-distance-hilbert-2026aAnalysisProbabilityDefines the quadratic Wasserstein distance between Borel probability measures with finite second moment on a Hilbert space.Couplings on a Hilbert Space: Tightness, Closedness under Weak Convergence, and Lower Semicontinuity of the Quadratic Cost
lemmalem:couplings-compactness-hilbert-2026aAnalysisProbabilityCouplings of tight families are tight, weak limits of couplings are couplings of the limits, and the quadratic cost is lower semicontinuous under weak convergence.Couplings on a Hilbert Space: Product Coupling, Swap, Finiteness of the Cost, Push-Forward Couplings, Modifying One Marginal, Quantisation, Gluing over a Finitely Supported Measure, the Lipschitz Bound and the Moment Bound
lemmalem:coupling-toolkit-hilbert-2026aAnalysisProbabilityBasic operations on couplings over a Hilbert space: product coupling, swap, finiteness of the cost, push-forward couplings, changing one marginal, quantisation onto finitely many points, gluing over a finitely supported measure, and Lipschitz and moment bounds.Couplings of Two Borel Probability Measures on a Hilbert Space and Their Quadratic Cost
definitiondef:coupling-quadratic-cost-hilbert-2026aAnalysisProbabilityDefines couplings of two Borel probability measures on a Hilbert space and the quadratic cost of a coupling.The Second Moment of a Borel Probability Measure on a Hilbert Space and the Probability Measures with Finite Second Moment
definitiondef:wasserstein-space-p2-hilbert-2026aAnalysisProbabilityDefines the second moment of a Borel probability measure on a Hilbert space and the set of those with finite second moment.Borel Sets of a Hilbert Space with an Orthonormal Basis: Coordinates, Determination by Finite-Dimensional Projections, and Pairs
lemmalem:borel-coordinates-hilbert-2026aAnalysisProbabilityOn a Hilbert space with an orthonormal basis, the coordinates generate the Borel sets, measurability can be tested coordinatewise, finite measures are determined by their finite-dimensional projections, and the Borel sets of the square are the product sigma-algebra.Weak Convergence of Finite Borel Measures is Preserved by Continuous Maps between Metric Spaces
lemmalem:weak-convergence-continuous-image-metric-2026aTopologyProbabilityPush-forward by a continuous map between metric spaces preserves weak convergence of finite Borel measures.Prokhorov's Theorem on a Metric Space: a Tight Sequence of Borel Probability Measures Has a Weakly Convergent Subsequence
theoremthm:prokhorov-tight-sequence-metric-2026aTopologyProbabilityA tight sequence of Borel probability measures on a metric space has a weakly convergent subsequence (direct half of Prokhorov's theorem).Ulam's Theorem: a Finite Borel Measure on a Complete Separable Metric Space is Tight
theoremthm:ulam-tightness-metric-2026aTopologyProbabilityEvery finite Borel measure on a complete separable metric space is tight (Ulam).Borel Probability Measures on a Real Hilbert Space with an Orthonormal Basis: Standing Notation
settingset:probability-measures-hilbert-2026aAnalysisProbabilityStanding notation for Borel probability measures on a real Hilbert space with a fixed orthonormal basis: coordinates, coordinate and synthesis maps, projections, Borel sets, push-forwards, pairs and weak convergence.At Each Cutoff the Lifted Wick-Square Solution Relative to the Free-Field Gaussian Is the Integral of the Galerkin Solution, and Its Pointwise Recovery Converges to the Renormalised Solution
corollarycor:lifted-wick-square-galerkin-identification-torus-2026aAnalysisProbabilityPDEAt each cutoff, the lifted Wick-square solution relative to the free-field Gaussian is the integral of the Galerkin solution; evaluating it along shrinking Gaussians recovers the Galerkin solution, and removing the cutoff afterwards gives the renormalised viscosity solution.The Galerkin Wick-Square Problem at a Cutoff as a Gaussian-Dressed Problem Relative to the Free-Field Gaussian: the Coupling Condition, the Riccati Coefficients, the Riccati Potential, the Profile and the Running Cost
lemmalem:wick-square-galerkin-gaussian-dictionary-torus-2026aAnalysisProbabilityPDEAt each cutoff, the Galerkin Wick-square data match the Gaussian dressing relative to the free-field Gaussian with temperature nu/2: the coupling condition holds, the dressing Riccati coefficients are twice the Galerkin ones, the Galerkin Riccati potential is the dressed Gaussian…The Lifted Ornstein-Uhlenbeck Hamilton-Jacobi Equation with a Linear Running Cost: Its Viscosity Solution Is the Integral of the Pointwise Solution, Which It Determines
theoremthm:lifted-ou-linear-cost-integral-representation-euclidean-2026aAnalysisProbabilityPDEFor a bounded uniformly continuous pointwise cost, the unique bounded viscosity solution of the lifted Ornstein-Uhlenbeck Hamilton-Jacobi equation with the integrated cost is the integral of the unique bounded viscosity solution of the pointwise equation, and the pointwise soluti…