Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Cyclically Monotone Subset of a Doubled Euclidean Space
definitiondef:cyclically-monotone-set-euclidean-2026aAnalysisA subset of a doubled Euclidean space is cyclically monotone when every finite cycle of its points has nonpositive chain sum.Absolutely Continuous Probability Measure on Euclidean Space
definitiondef:absolutely-continuous-probability-measure-euclidean-2026aAnalysisProbabilityA probability measure on Euclidean space is absolutely continuous when it gives measure zero to every Borel set of Lebesgue measure zero.The Support of a Borel Measure is Closed, and Carries Full Measure on a Separable Space
lemmalem:support-closed-full-measure-metric-2026aAnalysisThe support of a Borel measure on a metric space is closed, and on a separable space its complement is null.- Euclidean space with its usual distance has a countable dense subset.
Support of a Borel Measure on a Metric Space
definitiondef:support-borel-measure-metric-2026aAnalysisThe support of a Borel measure on a metric space is the set of points all of whose open balls have positive measure.A Comparison Principle for Viscosity Solutions on the Lift of the Wasserstein Space
theoremthm:comparison-lift-wasserstein-2026aAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair with closed score and an operator that is locally strictly proper and satisfies the shift-coercivity, shift-semicontinuity and second-order structure conditions, a bounded viscosity subsolution on the lift lies below a bounded viscosity sup…The Structure Estimate at a Maximiser of the Wasserstein-Doubled Difference on the Lift
lemmalem:comparison-estimate-lift-wasserstein-2026aAnalysisProbabilityPDEAt a maximiser of the Wasserstein-doubled difference of the delta-envelopes, the optimally coupled lift lies in the score domain, and the maximal value is bounded by the two moduli of a second-order structure pair evaluated at the penalised distance and at the scaled penalty.The Doubled Difference on the Lift of a Wasserstein-Coercive Penalty Pair: Bounds, Closed Superlevel Sets and the Least Penalty
lemmalem:doubled-difference-lift-wasserstein-2026aAnalysisProbabilityPDEFor a Wasserstein-coercive penalty pair, the penalty attains a least value, and the lifts of the delta-envelopes of a bounded upper semicontinuous function and a bounded lower semicontinuous function are bounded and have closed superlevel sets, as does the quadratically doubled d…Lifted Test Data from Second-Order Data on the Space of Square-Integrable Random Vectors: Compression along the Constant Tuple
lemmalem:compression-lifted-test-data-wasserstein-2026aAnalysisProbabilityPDEEvery function of class on the lift is a lifted test function whose translation Hessian is the compression of its Hilbert Hessian along the constant tuple; quadruples approximable by test data therefore produce lifted test functions with compressed matrices, and the second-…Compression of a Bounded Symmetric Bilinear Form along an Orthonormal Tuple
lemmalem:form-compression-hilbert-2026aAnalysisLinear AlgebraThe matrix of values of a bounded symmetric bilinear form on an orthonormal tuple is symmetric and its quadratic form is that of the original form along the span of the tuple; the compression is linear, does not increase the norm, preserves the order, sends the tail form to zero,…The Constant Tuple on : Coordinates, Projection, Tail Form, and Translation-Closed Preimages
lemmalem:constants-tuple-lift-wasserstein-2026aAnalysisProbabilityThe constant classes at the standard basis vectors form an orthonormal tuple in the space of square-integrable random vectors whose coordinate map is the mean of the law, whose projection is the constant class at that mean, and whose tail form is the centred second moment; preima…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…