Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Square-Integrable Tuples in a Tracial W*-Probability Space: Their Norm, Affine Images, Pairs, Embedded Images and Laws
definitiondef:l2-tuple-law-2026aAnalysisProbabilityAn L^2 tuple of a tracial W*-probability space is a tuple of vectors fixed by its conjugation; the definition fixes their L^2 norm, affine images, pairs and images under embeddings, and defines the law of an L^2 tuple as the L^2 law obtained as the limit of the laws of approximat…Laws of Self-Adjoint Tuples in a Tracial W*-Probability Space: Moments, Affine Images, Couplings, Embeddings and Approximation
lemmalem:bounded-tuple-laws-tracial-2026aAnalysisProbabilityThe law of a self-adjoint tuple in a tracial W*-probability space is a noncommutative law; its moments are inner products of vacuum vectors, affine images and embeddings behave as expected, the joint law of two tuples is a coupling whose cost is the squared L^2 distance, and laws…Self-Adjoint Tuples in a Tracial W*-Probability Space and Their Laws
definitiondef:bounded-tuple-law-tracial-2026aAnalysisProbabilityA self-adjoint d-tuple in a tracial W*-probability space is a d-tuple of self-adjoint elements of its algebra; its law is the functional on noncommutative polynomials given by the vacuum expectation of their values.The Noncommutative Laws with a Norm Bound Form a Complete Bounded Metric Space with Interpolation Points
theoremthm:nc-laws-complete-metric-2026aAnalysisProbabilityThe tracial states with norm bound R, with the noncommutative Wasserstein distance, form a complete and bounded metric space in which displacement interpolants are interpolation points.Moments of Noncommutative Laws are Lipschitz in the Wasserstein Distance
lemmalem:nc-moments-wasserstein-lipschitz-2026aAnalysisProbabilityOn laws with a norm bound, each moment is a Lipschitz function of the noncommutative Wasserstein distance; hence Wasserstein convergence implies weak-star convergence and sequentially weak-star closed sets are Wasserstein closed.The Noncommutative Wasserstein Distance Satisfies the Triangle Inequality and is a Metric on Noncommutative Laws
theoremthm:nc-wasserstein-triangle-2026aAnalysisProbabilityThe noncommutative quadratic Wasserstein distance satisfies the triangle inequality, so it is a metric on noncommutative laws and on each set of laws with a common norm bound.Gluing Two Noncommutative Couplings along a Common Marginal
lemmalem:nc-gluing-couplings-2026aAnalysisProbabilityTwo couplings sharing a middle marginal glue to a law of 3d variables with norm bound R whose first two and last two blocks have the given couplings, so its outer blocks couple the outer marginals.The Law of a Tuple of Bounded Self-Adjoint Operators in a Tracial Vector State
lemmalem:nc-law-operator-tuple-2026aAnalysisProbabilityA unit vector and a tuple of self-adjoint operators of norm at most R give a state on noncommutative polynomials with moment bounds R^k; if the vector state is tracial on products of words, this state is a noncommutative law with norm bound R.Noncommutative Laws, Couplings and the Wasserstein Distance: Standing Notation
settingset:nc-laws-2026bProbabilityStanding notation for noncommutative laws: polynomials, substitution and evaluation at operator tuples, laws and norm bounds, real and complex GNS spaces with their operators and tracial algebras, couplings and the Wasserstein metric, with the background results in force.The Noncommutative Wasserstein Distance: Existence of Optimal Couplings, Symmetry, Separation, a Moment Bound, Weak-Star Lower Semicontinuity, and Displacement Interpolation
theoremthm:nc-wasserstein-basic-2026aProbabilityOptimal couplings exist; the noncommutative Wasserstein distance is symmetric, vanishes exactly on the diagonal, is bounded by the second moments, is weak-star lower semicontinuous, and shrinks linearly along displacement interpolation.The Noncommutative Quadratic Wasserstein Distance and Optimal Couplings
definitiondef:nc-wasserstein-distance-2026aProbabilityDefines the noncommutative quadratic Wasserstein distance as the square root of the infimum of the cost over couplings, and optimal couplings as those attaining it.Couplings of Noncommutative Laws: the Norm Bound, the Cost Identity, the Tensor, Diagonal and Swapped Couplings, Weak-Star Closedness, and Displacement Interpolants
lemmalem:nc-coupling-basic-2026aProbabilityCouplings inherit the norm bound of their marginals, the cost is controlled by the second moments, the tensor, diagonal and swapped couplings exist, couplings are weak-star closed with continuous cost, and displacement interpolants are laws coupled to the endpoints at the expecte…Couplings of Two Noncommutative Laws and Their Quadratic Cost
definitiondef:nc-coupling-2026aProbabilityDefines couplings of two noncommutative laws as tracial states on twice as many variables with the given marginals, and the quadratic cost of a coupling.Sequential Weak-Star Compactness of the Noncommutative Laws with a Given Norm Bound
theoremthm:nc-laws-sequential-compactness-2026aTopologyProbabilityWeak-star convergence of laws is tested on monomials and has unique limits; the laws with a given norm bound are closed and sequentially compact.Weak-Star Convergence of Noncommutative Laws
definitiondef:weak-star-convergence-nc-laws-2026aTopologyProbabilityDefines weak-star convergence of a sequence of noncommutative laws as convergence of the values on every polynomial.- Defines the GNS space of a noncommutative law as the real Hilbert completion of the self-adjoint polynomials under the pairing given by the law.
The Norm Bound of a Noncommutative Law: Multiplication by a Variable is Bounded, the Bound is Detected by Even Moments, and Laws Pull Back under Self-Adjoint Substitutions
lemmalem:nc-law-multiplication-bound-2026aAlgebraProbabilityUnder a tracial state, multiplication by a self-adjoint polynomial with controlled even moments is bounded; the norm bound of a law is detected by the even moments of the variables, and laws pull back under self-adjoint and affine substitutions.Basic Properties of Noncommutative Laws: Adjoints, the Self-Adjoint Pairing, Cauchy-Schwarz, Monotonicity in the Bound, and Laws of Constant Tuples
lemmalem:nc-law-basic-2026aAlgebraProbabilityBasic properties of a tracial state: compatibility with adjoints, a real positive semidefinite pairing on self-adjoint polynomials, Cauchy-Schwarz, monotonicity of the bound sets, and the law of the zero tuple.Noncommutative Laws of Finitely Many Self-Adjoint Variables with a Norm Bound
definitiondef:nc-law-2026aAlgebraProbabilityDefines tracial states on noncommutative polynomials, their norm bounds, and noncommutative laws as tracial states with some norm bound.Mean-Field Limit of the N-Particle Dyson Game: the Value per Particle Converges to the Solution of the Dyson Hamilton-Jacobi Equation on the Wasserstein Space
theoremthm:dyson-n-particle-mean-field-limit-2026aAnalysisProbabilityPDEFor N particles on the line with logarithmic repulsion beta/(2(N-1)), a confining potential, idiosyncratic noise sigma^2/(N-1) below the collision threshold sigma^2 < beta and mean-field running cost, the solution of the N-particle Hamilton-Jacobi equation divided by N converges,…