Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.Continuous Mapping Theorem for Weak Convergence of Finite Borel Measures
lemmalem:weak-convergence-continuous-image-metric-2026bAnalysisProbabilityThe image measures under a continuous function between metric spaces of a weakly convergent sequence of finite Borel measures converge weakly to the image of the limit.Prokhorov's Theorem on a Metric Space: a Tight Sequence of Borel Probability Measures Has a Weakly Convergent Subsequence
theoremthm:prokhorov-tight-sequence-metric-2026bAnalysisProbabilityA tight sequence of Borel probability measures on a metric space has a subsequence converging weakly to a Borel probability measure (the 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-2026bAnalysisProbabilityEvery finite Borel measure on a complete separable metric space is tight (Ulam's theorem).A Closed Totally Bounded Subset of a Complete Metric Space is Compact
lemmalem:complete-totally-bounded-compact-metric-2026bTopologyIn a complete metric space, a totally bounded subset whose complement is open is sequentially compact and compact in the metric topology.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…Integrals of Lipschitz Semiconvex Viscosity Subsolutions and Lipschitz Semiconcave Viscosity Supersolutions of the Ornstein-Uhlenbeck Hamilton-Jacobi Equation Are Viscosity Sub- and Supersolutions of the Lifted Equation
propositionprop:semiconvex-lift-ou-hamilton-jacobi-euclidean-2026aAnalysisProbabilityPDEIntegrating a bounded Lipschitz semiconvex viscosity subsolution of the pointwise Ornstein-Uhlenbeck Hamilton-Jacobi equation against laws of finite relative entropy gives a viscosity subsolution of the lifted equation with the integrated running cost; semiconcave supersolutions…Penalised Extrema of the Integral of a Lipschitz Semiconvex Function Relative to the Gaussian Free-Energy Pair: Finite Relative Fisher Information and the First-Order Condition
lemmalem:semiconvex-integral-penalised-extrema-gaussian-euclidean-2026aAnalysisProbabilityIf the integral of a bounded Lipschitz semiconvex function, minus a multiple of the Gaussian free energy and an intrinsic test function, has a local maximum at a law, then that law has finite Fisher information relative to the Gaussian and the gradient of the function equals the…The Almost-Everywhere Gradient of a Lipschitz Semiconvex or Semiconcave Function Is Tangent at Every Absolutely Continuous Measure
lemmalem:semiconvex-gradient-tangent-wasserstein-2026aAnalysisProbabilityThe almost-everywhere gradient of a bounded Lipschitz function is a bounded Borel field defined off a null set of every absolutely continuous measure, and when the function is semiconvex or semiconcave this gradient lies in the Wasserstein tangent space at every absolutely contin…Sup- and Inf-Convolutions of Bounded Viscosity Sub- and Supersolutions of the Penalty-Drift Equation on the Whole Space with a Monotone Drift
lemmalem:sup-inf-convolution-monotone-drift-euclidean-2026aAnalysisPDEFor the penalty-drift equation on the whole space with a potential of monotone gradient, the sup-convolution of a bounded viscosity subsolution (inf-convolution of a bounded supersolution) is attained within a fixed radius, lies above (below) the function, is semiconvex (semiconc…Well-Posedness of the Lifted Hamilton-Jacobi Equation with a Wick-Square Cost Relative to a Diagonal Gaussian Measure, by Gaussian Dressing
theoremthm:lifted-wick-square-hamilton-jacobi-well-posed-euclidean-2026aAnalysisPDEFor the lifted Hamilton-Jacobi equation with a Wick-square cost relative to a diagonal Gaussian measure, viscosity solutions relative to the quadratic Riccati profile satisfy comparison, exist and are unique among functions differing from the profile by a bounded function; the di…Gaussian Dressing of the Wick-Square Cost: the Riccati Coefficients, the Dressed Variances, the Quadratic Profile, the Shifted Pair and the Shifted Operator
lemmalem:gaussian-dressing-wick-square-euclidean-2026aAnalysisPDESolving a scalar Riccati equation in each coordinate gives a quadratic profile and narrower dressed variances; the Gaussian free-energy pair of the dressed variances is the original pair shifted by the profile, and the lifted Wick-square operator shifted by the profile is the lif…