Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.Positive Semidefinite Kernels on a Finite Set: Rank-One Decomposition and the Schur Product
lemmalem:psd-kernel-finite-set-2026aLinear AlgebraSums of rank-one kernels are positive semidefinite, every positive semidefinite kernel on an N-element set is a sum of N rank-one kernels, and the entrywise (Schur) product of two positive semidefinite kernels is positive semidefinite.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.The Hilbert Completion is a Real Hilbert Space Containing a Dense Isometric Image, and Bounded Linear Maps Extend to It
theoremthm:hilbert-completion-semi-inner-product-2026aAnalysisThe Hilbert completion is a real Hilbert space into which the original space maps isometrically with dense image, and bounded linear maps extend uniquely to it.The Hilbert Completion of a Real Vector Space with a Positive Semidefinite Symmetric Bilinear Form
definitiondef:hilbert-completion-semi-inner-product-2026aAnalysisDefines the Hilbert completion of a real vector space with a positive semidefinite symmetric bilinear form, as cosets of Cauchy sequences modulo null sequences, with its canonical map.Cauchy Sequences for a Positive Semidefinite Symmetric Bilinear Form: Cauchy-Schwarz, the Space of Cauchy Sequences, Convergence of Pairings, and Null Sequences
lemmalem:semi-inner-product-cauchy-sequences-2026aAnalysisFor a positive semidefinite symmetric bilinear form: Cauchy-Schwarz, the vector space of Cauchy sequences, convergence of pairings, null sequences and their cosets.Substitution is the Unique Unital Homomorphism with Prescribed Values on the Variables: Monomials, Products, Adjoints and Composition
lemmalem:nc-polynomial-substitution-basic-2026aAlgebraSubstitution is the unique unital algebra homomorphism with prescribed values on the variables; it respects adjoints when the substituted polynomials are self-adjoint and composes as expected.Substitution of Noncommutative Polynomials into the Variables
definitiondef:nc-polynomial-substitution-2026aAlgebraDefines the substitution of a tuple of polynomials into the variables of a noncommutative polynomial.Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts
lemmalem:nc-polynomials-algebra-2026aAlgebraThe noncommutative polynomials form a unital complex algebra with an involution; linear maps are determined by their values on monomials, and every polynomial splits uniquely into self-adjoint real and imaginary parts.The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables
definitiondef:nc-polynomials-2026aAlgebraDefines the noncommutative polynomials in n self-adjoint variables as finitely supported coefficient functions on words, with the convolution product, monomials and the adjoint.Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability
lemmalem:words-finite-alphabet-basic-2026aCombinatoricsWords form a monoid under concatenation, reversal is an anti-multiplicative involution, every word has finitely many factorisations, and the set of words is countable.Words over a Finite Alphabet: the Empty Word, Concatenation and Reversal
definitiondef:words-finite-alphabet-2026bCombinatoricsDefines the words in finitely many letters, including the empty word, together with concatenation and reversal.Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus
lemmalem:finite-set-indexed-sum-toolkit-2026aAlgebraElementary facts about sums over finite index sets: finite unions of finite sets are finite, sums split over disjoint unions, vanishing terms can be dropped, double sums over dependent pairs, and conjugation and the modulus of complex sums.Cesaro Means of a Convergent Real Sequence Converge to Its Limit
lemmalem:cesaro-mean-real-2026bAnalysisIf a sequence of real numbers converges to a, then the averages of its first m terms converge to a as well.