Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Half the Squared Torus Wasserstein Distance to a Fixed Measure: the One-Sided Bound Along Couplings, Differentiability at an Absolutely Continuous Source, and the Tangent Gradient
lemmalem:torus-squared-distance-2026aAnalysisProbabilityHalf the squared torus Wasserstein distance to a fixed measure lies below its first-order expansion plus half the cost along every coupling out of a mapped source; at an absolutely continuous source it is differentiable along couplings with gradient minus the optimal displacement…Intrinsic Test Functions on the Torus Wasserstein Space
definitiondef:torus-intrinsic-test-function-2026aAnalysisProbabilityAn intrinsic test function on a set of probability measures on the torus is a continuous function that is differentiable along couplings at every measure of the set with gradient in the tangent space, the gradients varying continuously along couplings of vanishing torus cost.Differentiability Along Couplings of a Function on the Torus Wasserstein Space, and Its Gradient
definitiondef:torus-differentiable-along-couplings-2026aAnalysisProbabilityA function on the probability measures on the torus is differentiable along couplings at a measure with a given gradient field when its increment along every coupling of small torus cost equals the displacement pairing of that field up to an error small relative to the square roo…The Torus Displacement Pairing: Linearity, the Cost Bound, and Vanishing of a Field with First-Order Small Pairings
lemmalem:torus-displacement-pairing-2026aAnalysisProbabilityThe torus displacement pairing is linear in the field and bounded by the norm of the field times the square root of the torus cost; a field whose pairings along all couplings of small cost are small relative to the square root of the cost is zero.The Torus Displacement Pairing of a Vector Field Along a Coupling
definitiondef:torus-displacement-pairing-2026aAnalysisProbabilityThe torus displacement pairing of a square-integrable vector field along a coupling integrates the dot product of the field at the first point with the wrapped displacement from the first point to the second.Finite Torus Fisher Information, the Torus Score and the Torus Fisher Information of a Probability Measure on the Torus
definitiondef:torus-score-fisher-2026aAnalysisProbabilityA probability measure on the torus has finite torus Fisher information when integrals of Laplacians of smooth periodic functions are bounded by the norm of their gradients; its score is the tangent vector representing minus that integral, and its Fisher information is the squared…The Torus Tangent Space: Linearity of the Periodic Calculus, Closed Subspace, and Representation of Bounded Functionals on Gradients
lemmalem:torus-tangent-space-basic-2026aAnalysisProbabilitySmooth periodic functions form a vector space on which gradient and Laplacian are linear; their gradients form a subspace whose closure, the torus tangent space, is a closed subspace; and a linear functional on smooth periodic functions bounded by the norm of the gradient is repr…The Tangent Space of the Torus Wasserstein Space at a Probability Measure
definitiondef:torus-tangent-space-2026aAnalysisProbabilityThe tangent space at a probability measure on the torus is the closure, in the square-integrable vector fields against that measure, of the gradients of smooth periodic functions.Optimal Transport on the Flat Torus: Standing Notation
settingset:torus-wasserstein-2026aAnalysisProbabilityFixes the notation for optimal transport on the flat torus: the wrapped displacement and torus distance, probability measures on the torus with the torus cost, Wasserstein distance and optimal couplings, and optimal maps with their displacement fields, and puts the basic results…Stability of the Optimal Map and of the Displacement on the Torus Along Couplings of Nearly Optimal Cost
theoremthm:torus-optimal-map-stability-2026aAnalysisProbabilityAlong any sequence of couplings of a uniquely mapped pair on the torus whose torus costs converge to the optimal cost, the second point converges in mean square to the image of the first under the optimal map; if the source is absolutely continuous, the wrapped displacement of th…McCann's Theorem on the Flat Torus: Optimal Couplings out of an Absolutely Continuous Measure are Induced by a Unique Map with a Periodic Potential
theoremthm:torus-optimal-map-2026aAnalysisProbabilityIf the source measure on the flat torus is absolutely continuous, the pair is uniquely mapped on the torus; almost every displacement of an optimal map is the unique shortest one and is given by the subgradient of a convex function whose difference from half the squared norm is p…Optimal Maps on the Torus, Uniquely Mapped Pairs and the Displacement Field of a Map
definitiondef:torus-optimal-map-2026aAnalysisProbabilityA Borel map is an optimal map on the torus from one measure to another when it pushes the first onto the second and the coupling it induces is optimal for the torus cost; a pair is uniquely mapped when some optimal map induces every optimal coupling; the displacement field of a m…The Support of an Optimal Coupling on the Torus is Torus-Cyclically Monotone
lemmalem:torus-optimal-coupling-cyclically-monotone-2026aAnalysisProbabilityThe support of an optimal coupling of two probability measures on the flat torus is torus-cyclically monotone.The Torus Wasserstein Space is a Sequentially Compact Metric Space in which Optimal Couplings Exist
theoremthm:torus-wasserstein-compact-2026aAnalysisProbabilityAny two probability measures on the flat torus have an optimal coupling; the torus Wasserstein distance is a metric on the probability measures on the torus; and every sequence of such measures has a subsequence converging in that metric.The Torus Wasserstein Distance: Comparison with the Euclidean Distance, Wrapping, and Integrals of Periodic Functions
lemmalem:torus-wasserstein-basic-2026aAnalysisProbabilityMeasures on the flat torus have finite second moment; the torus cost of a coupling is at most its Euclidean quadratic cost; wrapping two measures on Euclidean space does not increase their Wasserstein distance; and integrals of continuous periodic functions depend continuously, a…Probability Measures on the Flat Torus, the Torus Cost of a Coupling, the Torus Wasserstein Distance and Optimal Couplings
definitiondef:torus-wasserstein-distance-2026aAnalysisProbabilityProbability measures on the flat torus are Borel probability measures on Euclidean space carried by the half-open unit cell; the torus cost of a coupling integrates the squared flat torus distance, the torus Wasserstein distance is the square root of the least cost, and a couplin…Tracial W*-Probability Spaces and Square-Integrable Tuples: Standing Notation
settingset:tracial-w-star-l2-2026aAnalysisProbabilityStanding notation for tracial W*-probability spaces, their traces, conjugations and self-adjoint vectors, trace-preserving embeddings, self-adjoint and L^2 tuples and their laws, with the basic results on them in force.Every Square-Integrable Noncommutative Law is the Law of a Square-Integrable Tuple; Realisation of Couplings and of Almost Optimal Pairs
theoremthm:l2-law-realisation-2026aAnalysisProbabilityEvery L^2 noncommutative law is the law of an L^2 tuple in some tracial W*-probability space; likewise every L^2 law of 2d variables is the law of a pair of L^2 tuples, and any two L^2 laws are the laws of two tuples in a common space whose squared L^2 distance is within any marg…Gluing a Chain of Noncommutative Couplings into Consistent Joint Laws
lemmalem:nc-chain-gluing-2026aAnalysisProbabilityGiven a sequence of noncommutative laws and couplings between consecutive terms, there is a consistent sequence of joint laws of the first k blocks of variables whose consecutive pairs of blocks have the given couplings as laws.Calculus of Laws of Square-Integrable Tuples: Bounded Tuples, the Lipschitz Bound, Moments, Affine Push-Forwards, Couplings and Embeddings
lemmalem:l2-tuple-law-properties-2026aAnalysisProbabilityThe law of an L^2 tuple extends the law of bounded self-adjoint tuples, is 1-Lipschitz for the L^2 norm, has its moments given by inner products, commutes with affine push-forwards, turns pairs into L^2 couplings whose cost is the squared L^2 distance, and is invariant under trac…