Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- A confining potential on the real line is a convex function of class C^2 that grows faster than every multiple of x^2, whose derivative is bounded by a multiple of one plus its absolute value, and whose second derivative is small against its absolute value.
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.The Structure Estimate at a Maximiser of the Wasserstein-Doubled Difference
lemmalem:comparison-estimate-wasserstein-2026dAnalysisPDEFor a bounded-above viscosity subsolution and a bounded-below viscosity supersolution on the penalty domain, a nonnegative supremum of the Wasserstein-doubled difference of their delta-envelopes is attained at a pair in the score domain at which the properness constant times the…Intrinsic Test Functions at a Maximiser of the Wasserstein-Doubled Difference
lemmalem:doubling-test-functions-wasserstein-2026cAnalysisPDEAt a maximiser of the Wasserstein-doubled difference of the delta-envelopes of two bounded functions over a penalty domain with the map property, there is a maximising pair and a pair of matrices admitted by Ishii's lemma such that each side is touched, arbitrarily close by, by i…A Triangle Inequality for Discrepancies Along a Composite Coupling
lemmalem:discrepancy-gluing-wasserstein-2026aAnalysisProbabilityAlong the composite of two couplings obtained by gluing, the square root of the discrepancy between a field on the first measure and a field on the third is at most the sum of the square roots of the discrepancies through any field on the middle measure.The Displacement Midpoint and the Midpoint Split of the Squared Wasserstein Distance
lemmalem:midpoint-split-wasserstein-2026aAnalysisProbabilityThe midpoint of an optimal coupling of two measures lies at a quarter of their squared distance from each, and the squared Wasserstein distance between any two measures is bounded by twice the centred squared distances of each to that midpoint plus the squared distance of their m…A Comparison Principle for Viscosity Solutions on the Wasserstein Space
theoremthm:comparison-wasserstein-2026dAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair with closed score along couplings whose penalty domain has the map property, and an operator that is locally strictly proper and satisfies the shift-coercivity, shift-semicontinuity and second-order structure conditions: if u is a viscosity…