Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.A Closed Totally Bounded Subset of a Complete Metric Space is Compact
lemmalem:complete-totally-bounded-compact-metric-2026aAnalysisTopologyA closed, totally bounded subset of a complete metric space is sequentially compact and compact.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…The Lifted Hamilton-Jacobi Equation with a Wick-Square Cost Relative to a Diagonal Gaussian Measure
equationeq:lifted-wick-square-hamilton-jacobi-euclidean-2026aAnalysisPDEThe lifted Ornstein-Uhlenbeck Hamilton-Jacobi equation relative to a diagonal Gaussian measure whose running cost is the integral of a Wick-square potential plus a function on measures; viscosity solutions are taken relative to the Gaussian free-energy pair and a profile.Shifting the Penalised Viscosity Notion by an Intrinsic Test Function: Composition of Shifts, the Shift Identity, Invariance under a Change of Profile, and a Change of the Penalty
lemmalem:profile-shift-viscosity-wasserstein-2026aAnalysisPDESubtracting an intrinsic test function from a function and shifting the operator accordingly preserves being a penalised viscosity subsolution or supersolution; consequently the notion relative to a profile does not depend on the profile within a growth class, and a penalty chang…The Wick-Square Potential Relative to a Diagonal Gaussian Measure
definitiondef:wick-square-potential-diagonal-gaussian-euclidean-2026aAnalysisProbabilityThe Wick-square potential with variances c and couplings beta is the sum over coordinates of beta_i times x_i squared minus c_i: each square with its mean under the diagonal Gaussian measure removed.Viscosity Subsolutions, Supersolutions and Solutions Relative to a Penalty Pair and a Profile
definitiondef:profile-viscosity-solution-wasserstein-2026aAnalysisPDEGiven a penalty pair, an equation operator and an intrinsic test function called the profile, a function is a viscosity subsolution, supersolution or solution relative to the profile when its difference with the profile is one, in the penalised sense, of the operator shifted by t…