Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Subsets of a Real Hilbert Space Translation-Closed along an Orthonormal Tuple
definitiondef:translation-closed-subset-hilbert-2026aAnalysisA nonempty subset of a real Hilbert space is translation-closed along an orthonormal tuple if adding any vector in the span of the tuple keeps a point of the subset inside it.Lions' Lemma on a Hilbert Space over a Translation-Closed Set: Test Data and Form Bounds at a Sequentially Strict Maximum of a Quadratically Penalised Difference
lemmalem:lions-doubling-translation-closed-hilbert-2026aAnalysisPDEThe infinite-dimensional counterpart of Ishii's lemma, carried from a linear subspace to any set closed under the translations of a finite orthonormal tuple: at a sequentially strict maximum of a quadratically penalised difference, both functions admit test data whose second-orde…Fibre Suprema along a Coordinate Map over a Translation-Closed Set and Their Semicontinuous Envelopes
lemmalem:fibre-supremum-envelope-translation-closed-hilbert-2026aAnalysisTaking suprema and infima over the fibres of a coordinate map turns a quadratically penalised difference on a set closed under the translations of the tuple into one on Euclidean space whose semicontinuous envelopes still attain their maximum at the image of the original maximum…Existence of an Optimal Coupling of Two Probability Measures with Finite Second Moment
theoremthm:optimal-coupling-exists-euclidean-2026aAnalysisProbabilityAny two probability measures on Euclidean space with finite second moment admit an optimal coupling: the infimum defining the quadratic Wasserstein distance is attained.The Couplings of Two Probability Measures on Euclidean Space are Closed under Weak Convergence
lemmalem:couplings-weakly-closed-euclidean-2026aAnalysisProbabilityA weak limit of couplings of two fixed probability measures on Euclidean space is again a coupling of them.Continuity of the Coordinate Projections and of the Quadratic Cost Function, and Passage of a Cost Bound to a Weak Limit
lemmalem:quadratic-cost-lsc-weak-euclidean-2026aAnalysisProbabilityThe coordinate projections of a Euclidean product are nonexpansive and the quadratic cost function is continuous; consequently a bound on the quadratic cost that holds along a weakly convergent sequence of probability measures holds in the limit.Tightness from Bounded Second Moments, and Tightness of the Couplings of Two Measures with Finite Second Moment
lemmalem:tightness-criteria-euclidean-2026aAnalysisProbabilityA family of probability measures on Euclidean space with uniformly bounded second moments is tight; the second moment of a coupling is the sum of the second moments of its marginals, so the couplings of two measures with finite second moment form a tight family.Prokhorov's Theorem on Euclidean Space: a Tight Sequence of Probability Measures Has a Weakly Convergent Subsequence
theoremthm:prokhorov-sequential-euclidean-2026aAnalysisProbabilityEvery tight sequence of Borel probability measures on a Euclidean space has a subsequence converging weakly to a Borel probability measure on that space.The Radial Compactification of Euclidean Space: Norm Continuity, a Homeomorphism onto the Open Unit Ball, Radial Cutoffs, and Extension of Test Functions
lemmalem:radial-compactification-euclidean-2026aAnalysisTopologyThe map sending x to x divided by one plus its norm is a homeomorphism of Euclidean space onto the open unit ball; compact sets are carried into balls of radius less than one, radial cutoffs are available there, and multiplying a continuous function by such a cutoff produces a co…Tight Family of Borel Measures on a Metric Space
definitiondef:tight-family-borel-measures-metric-2026bAnalysisProbabilityA family of finite Borel measures on a metric space is tight when, for every tolerance, one compact set carries all but less than that tolerance of the mass of every member.The Metric Subspace: Continuity, the Borel Sigma-Algebra, and the Restriction of a Borel Measure
lemmalem:borel-subspace-metric-2026aAnalysisTopologyThe Borel sets of a metric subspace are the traces of the ambient Borel sets; when the subspace is itself Borel they are the ambient Borel sets it contains, the restriction of a Borel measure is a Borel measure on it, and an integral of a function vanishing off the subspace is co…Compact Subsets of a Metric Space are Closed and Borel
lemmalem:compact-subset-closed-borel-metric-2026aAnalysisTopologyA compact subset of a metric space is closed, and therefore belongs to the Borel sigma-algebra, as does its complement.Optimally Coupled Pairs of Square-Integrable Random Vectors
definitiondef:optimally-coupled-pair-wasserstein-2026aAnalysisProbabilityTwo square-integrable random vectors are optimally coupled if their joint law is an optimal coupling of their laws, that is, if their mean-square distance equals the Wasserstein distance of their laws.Second-Order Equation Operators on the Lift of the Wasserstein Space and Their Delta-Shifts
definitiondef:operator-lift-wasserstein-2026aAnalysisProbabilityA second-order equation operator on the lift takes a square-integrable random vector whose law lies in a given set of measures, a real number, a second random vector, and a symmetric matrix, and depends on the two random vectors only through their joint law. Its delta-shifts rela…The Joint Law of Two Classes of Square-Integrable Random Vectors: Marginals, Cost, and Invariance Under Shifts by a Vector Field
lemmalem:joint-law-random-vectors-wasserstein-2026aAnalysisProbabilityTwo classes of square-integrable random vectors have a well-defined joint law with finite second moment, whose marginals are their laws and which is a coupling of them with cost the mean-square distance; equality of joint laws is preserved when the same vector field of the common…Existence, Penalty Bounds and Optimal Realisation at a Maximiser of the Wasserstein-Doubled Difference on the Lift
lemmalem:doubling-maximiser-lift-wasserstein-2026bAnalysisPDEFor a Wasserstein-coercive pair the Wasserstein-doubled difference of the delta-envelopes attains its supremum, the penalty and second moment are bounded at a near-maximiser independently of the doubling strength, the penalised distance vanishes along a doubling sequence, and the…Penalty Pairs with Closed Score
definitiondef:closed-score-penalty-pair-wasserstein-2026bAnalysisProbabilityA penalty pair has closed score if, along any sequence of random vectors converging in mean square whose scores are uniformly bounded, the limit law lies in the score domain and the scores converge weakly to the score at the limit.Basic Properties of a Wasserstein-Coercive Penalty Pair
lemmalem:w2-coercive-penalty-pair-basic-wasserstein-2026cAnalysisProbabilityFor a Wasserstein-coercive penalty pair the second moment is bounded on each sublevel set of the penalty, and the penalty is bounded below and lower semicontinuous.Wasserstein-Coercive Penalty Pairs
definitiondef:w2-coercive-penalty-pair-wasserstein-2026cAnalysisProbabilityA penalty pair is Wasserstein-coercive if every sublevel set of its penalty is sequentially compact for the Wasserstein distance.Viscosity Subsolution, Supersolution and Solution on the Lift of the Wasserstein Space
definitiondef:viscosity-lift-wasserstein-2026bAnalysisPDEA bounded-near-each-point function on the Wasserstein space is a viscosity subsolution (supersolution) on the lift if, wherever its delta-envelope composed with the law map minus a lifted test function has a local maximum (minimum) on the lift of the penalty domain, the shifted o…