Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Well-Posedness of the Dyson Hamilton-Jacobi Equation with Common Noise and a Confining Potential: Existence and Uniqueness of a Bounded Viscosity Solution
theoremthm:dyson-confined-well-posed-wasserstein-2026bAnalysisProbabilityPDEFor a confining potential and a bounded uniformly continuous running cost, the Dyson Hamilton-Jacobi equation with common noise satisfies comparison for bounded sub- and supersolutions and has exactly one bounded viscosity solution, which lies between plus and minus the cost boun…The Dyson Hamilton-Jacobi Equation with Common Noise and a Confining Potential on the Wasserstein Space of the Real Line
equationeq:dyson-confined-hamilton-jacobi-wasserstein-2026bAnalysisProbabilityPDEThe discounted Dyson Hamilton-Jacobi equation with common noise and a confining potential V on the Wasserstein space of the real line, the penalty-drift equation of the confined logarithmic-energy pair with unit control cost.The Hamilton-Jacobi Operator with Common Noise and Penalty Drift Satisfies the Hypotheses of the Comparison Principle for a Displacement Convex Pair
lemmalem:penalty-drift-comparison-hypotheses-wasserstein-2026cAnalysisProbabilityPDEFor a displacement convex penalty pair whose penalty controls the second moment and the common-noise contraction of the translation Hessian, control cost at most one and a bounded uniformly continuous running cost, the Hamilton-Jacobi operator with common noise along a matrix and…The Confined Logarithmic-Energy Pair is a Displacement Convex, Wasserstein-Coercive Penalty Pair with Closed Score and Regular Penalised Maxima
lemmalem:confined-log-energy-pair-properties-line-2026bAnalysisProbabilityThe confined logarithmic-energy pair is a Wasserstein-coercive, displacement convex penalty pair with closed score and regular penalised maxima, whose domain has the map property; its penalty is lower semicontinuous and controls the second moment and the translation Hessian, whic…The Confined Logarithmic-Energy Pair on the Wasserstein Space of the Real Line
definitiondef:confined-log-energy-pair-line-2026bAnalysisProbabilityThe confined logarithmic-energy pair on the real line: penalty a quarter of the inverse temperature times the logarithmic energy plus the integral of a confining potential V, with score V' minus a quarter of the inverse temperature times the free score.Splitting a Bounded First Variation into a Square-Integrable Potential Force and a Finite Free Fisher Information
lemmalem:confined-score-splitting-line-2026aAnalysisProbabilityFor a confining potential V and an atomless measure of finite logarithmic energy, if the first variation of V minus a multiple of the logarithmic energy is bounded in L^2, then V' is square-integrable and the measure has finite free Fisher information.Displacement Convexity of the Logarithmic Energy on the Real Line
lemmalem:logarithmic-energy-displacement-convex-line-2026aAnalysisProbabilityOn the real line the logarithmic energy lies above its tangent along optimal couplings: at a measure of finite free Fisher information, the energy plus the displacement pairing of minus the free score is at most the energy of the target.A Probability Measure on the Real Line with a Continuously Differentiable Density of Bounded Derivative Has Finite Free Fisher Information and Finite Logarithmic Energy
lemmalem:free-fisher-smooth-density-line-2026aAnalysisProbabilityA probability measure on the real line with finite second moment and a continuously differentiable density of bounded derivative has finite free Fisher information and finite logarithmic energy.The First Variation of the Logarithmic Energy on the Real Line along Gradient Perturbations of the Identity
lemmalem:logarithmic-energy-first-variation-line-2026aAnalysisProbabilityAlong the push-forward by the identity plus a small multiple of the derivative of a test function, the logarithmic energy is differentiable at zero with derivative minus the double integral of the difference quotient, which is minus the pairing with the free score when the free F…Basic Properties of the Logarithmic Energy on the Real Line: Lower Bound, Translation Invariance, Closed Sublevel Sets and Lower Semicontinuity
lemmalem:logarithmic-energy-basic-line-2026aAnalysisProbabilityThe logarithmic energy is bounded below by minus one minus the second moment, is invariant under translations, has sublevel sets closed under Wasserstein convergence, and is lower semicontinuous.The Logarithmic Energy of a Probability Measure on the Real Line
definitiondef:logarithmic-energy-line-2026aAnalysisProbabilityThe logarithmic energy of an atomless probability measure on the real line with finite second moment is the double integral of -log|x-y|, defined on the measures for which that kernel is integrable.Wasserstein Convergence from Weak Convergence with Uniformly Integrable Second Moments, and Wasserstein Compactness under a Superquadratic Moment Bound
lemmalem:w2-compactness-superquadratic-moment-euclidean-2026aAnalysisProbabilityWeak convergence together with uniformly integrable second moments gives convergence in the Wasserstein distance, and a uniform bound on a superquadratic moment gives a Wasserstein-convergent subsequence.Uniqueness and Continuity on Energy Sublevel Sets of Bounded Viscosity Solutions on the Wasserstein Space
corollarycor:comparison-uniqueness-continuity-wasserstein-2026bAnalysisProbabilityPDEUnder the hypotheses of the comparison principle, two bounded viscosity solutions coincide on the penalty domain, and a bounded viscosity solution is uniformly continuous in the Wasserstein distance on every sublevel set of the penalty.The Delta-Envelopes of Bounded Functions and Their Monotonicity in the Weight, for a Wasserstein-Closed Penalty Pair
lemmalem:delta-envelopes-bounded-wasserstein-2026bAnalysisProbabilityPDEFor a Wasserstein-closed penalty pair, a function bounded above on the penalty domain has penalty-subordinate growth from above and its delta-envelope lies below the bound minus delta times the penalty; and increasing the weight from delta to delta' lowers the upper envelope by a…Penalty-Subordinate Growth of a Function on the Penalty Domain
definitiondef:penalty-subordinate-growth-wasserstein-2026aAnalysisProbabilityA function on the penalty domain has penalty-subordinate growth from above if, for every positive delta, it is bounded above by a constant plus delta times the penalty; growth from below is the mirror condition.Perron's Method on the Wasserstein Space: Existence of a Viscosity Solution Between a Subsolution and a Supersolution
theoremthm:perron-existence-wasserstein-2026cAnalysisProbabilityPDEFor a Wasserstein-closed penalty pair with regular penalised maxima whose penalty domain has the map property, and a degenerate elliptic operator, the pointwise supremum of all viscosity subsolutions on the penalty domain lying between a given subsolution and a given supersolutio…The Bump Construction on the Wasserstein Space: the Local Maximum of a Viscosity Subsolution and a Penalised Intrinsic Test Function
lemmalem:perron-bump-wasserstein-2026cAnalysisProbabilityPDEInside a Wasserstein ball, replace a viscosity subsolution v on the penalty domain by the maximum of v and an intrinsic test function, bounded above on the ball, minus a multiple of the penalty, which stays below v near the edge of the ball. If the test function satisfies the shi…The Pointwise Supremum of a Uniformly Subordinate Family of Viscosity Subsolutions on the Wasserstein Space is a Viscosity Subsolution
lemmalem:sup-of-subsolutions-wasserstein-2026cAnalysisProbabilityPDEFor a Wasserstein-closed penalty pair whose penalty domain has the map property, the pointwise supremum of a nonempty family of viscosity subsolutions on the penalty domain that is uniformly subordinate from above (for each positive delta, one constant plus delta times the penalt…Attained Maxima on Closed Balls of the Penalty Domain, for a Wasserstein-Coercive Penalty Pair
lemmalem:penalised-usc-attains-ball-wasserstein-2026bAnalysisProbabilityFor a Wasserstein-coercive penalty pair, an upper semicontinuous function on the penalty domain that lies below a constant minus a positive multiple of the penalty on a closed ball attains its supremum on that ball.Penalty Pairs with Regular Penalised Maxima
definitiondef:regular-penalised-maxima-wasserstein-2026bAnalysisProbabilityPDEA penalty pair has regular penalised maxima when every local maximiser, on the penalty domain, of an intrinsic test function minus a positive multiple of the penalty lies in the score domain.