Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Space of Square-Integrable Maps from a Measure Space into a Hilbert Space with an Orthonormal Basis
definitiondef:square-integrable-maps-hilbert-valued-2026aProbabilityDefines the space of almost-everywhere classes of square-integrable maps from a measure space into a Hilbert space with an orthonormal basis, with pointwise operations and the integrated inner product.Measurable Maps into a Hilbert Space with an Orthonormal Basis: Norms, Inner Products and Linear Combinations, Synthesis from Coordinates, Square-Integrability, and Almost-Everywhere Equality
lemmalem:measurable-maps-hilbert-valued-2026aProbabilityMeasurable maps into a Hilbert space with an orthonormal basis are closed under linear combinations and have measurable norms, inner products and coordinates; square-summable measurable coordinates synthesise a measurable map; square-integrable maps have integrable inner products…Relative Entropy with Respect to a Diagonal Gaussian Measure on a Hilbert Space: the Moment Bound, the Cutoff Projections, and Bounded, Tight, Weakly Closed, Wasserstein-Closed and Weakly Sequentially Compact Sublevel Sets
propositionprop:relative-entropy-diagonal-gaussian-hilbert-2026aProbabilityRelative to a diagonal Gaussian measure on a Hilbert space, finite relative entropy implies finite second moment with a linear bound, the entropy is the limit of the entropies of the finite-dimensional cutoffs, and entropy sublevel sets are bounded, tight, weakly closed, Wasserst…Relative Entropy of the Finite-Dimensional Projections of Borel Probability Measures on a Hilbert Space: Monotonicity and Approximation
lemmalem:relative-entropy-projections-hilbert-2026aProbabilityFor Borel probability measures on a Hilbert space with an orthonormal basis, the relative entropies of the projections to the first n coordinates are nondecreasing in n, and the relative entropy is finite exactly when they are bounded, in which case it is their limit.Relative Entropy on a Metric Space: the Variational Criterion over Bounded Lipschitz Functions and Sequentially Closed Sublevel Sets under Weak Convergence
lemmalem:relative-entropy-weak-closed-metric-2026aProbabilityOn a metric space it suffices to test the variational criterion for relative entropy against bounded Lipschitz functions; consequently sublevel sets of the relative entropy are sequentially closed under weak convergence.Relative Entropy on a Measurable Space: the Gibbs Inequality, the Variational Criterion and Formula, the Entropy Inequality, Small Sets and Data Processing
lemmalem:relative-entropy-variational-measurable-2026aProbabilityOn any measurable space, relative entropy dominates the Donsker-Varadhan functional of every bounded measurable test function and equals its supremum; a uniform bound on that functional forces finite relative entropy. Consequences: the entropy inequality, a bound on the mass of s…- A variance sequence is a sequence of positive reals with convergent series; its truncation to the first n terms is a variance vector, with the associated diagonal Gaussian measure on n-dimensional Euclidean space.
Gaussian Integration by Parts for Functions of Finitely Many Coordinates Relative to a Diagonal Gaussian Measure on a Hilbert Space
theoremthm:gaussian-integration-by-parts-hilbert-2026aProbabilityFor a function of the first n coordinates with a gradient of at most linear growth, the integral of a coordinate derivative against a diagonal Gaussian measure equals the integral of the function times the coordinate divided by its variance, and the derivative along a Cameron-Mar…The Cameron-Martin Translation Formula for a Diagonal Gaussian Measure on a Hilbert Space
theoremthm:cameron-martin-translation-hilbert-2026aProbabilityTranslating a diagonal Gaussian measure by a Cameron-Martin vector h produces the measure with density exp of the Paley-Wiener functional of h minus half the Cameron-Martin square of h.The Paley-Wiener Functional of a Cameron-Martin Vector: Borel Measurability, Almost Everywhere and Mean-Square Convergence, Mean Zero and Variance the Cameron-Martin Square
lemmalem:paley-wiener-functional-hilbert-2026aProbabilityThe Paley-Wiener functional is Borel and equals the scaled coordinate for basis vectors; for a Cameron-Martin vector its partial sums converge almost everywhere and in mean square under the diagonal Gaussian measure, and its mean is zero and its second moment the Cameron-Martin s…The Paley-Wiener Functional of a Vector Relative to a Variance Sequence
definitiondef:paley-wiener-functional-hilbert-2026aProbabilityFor a variance sequence and a vector h, the Paley-Wiener partial sums are the finite sums of the coordinates of h times those of x divided by the variances, and the Paley-Wiener functional is their limit where it exists and zero elsewhere.The Cameron-Martin Space of a Diagonal Gaussian Measure on a Hilbert Space
definitiondef:cameron-martin-space-hilbert-2026aProbabilityThe Cameron-Martin space of a variance sequence consists of the vectors whose squared coordinates divided by the variances form a convergent series, and the Cameron-Martin square is the sum of that series.Moments of a Diagonal Gaussian Measure on a Hilbert Space: Coordinate Covariances, Finite Second Moment, and Exponential Moments of the Squared Norm
lemmalem:diagonal-gaussian-measure-moments-hilbert-2026aProbabilityUnder a diagonal Gaussian measure the coordinates are centred and uncorrelated with variances given by the variance sequence, the second moment is the sum of the variances, and the squared norm has exponential moments below the threshold set by the largest variance.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.