Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Locally Lipschitz Function on an Open Subset of a Metric Space
definitiondef:locally-lipschitz-metric-2026bAnalysisDefines a real-valued function on an open subset of a metric space to be locally Lipschitz when each point has an open ball in the subset on which the function satisfies a Lipschitz bound.- A metric space has interpolation points if any two points x, y have, for each t in [0,1], a point at distance at most t d(x,y) from x and at most (1-t) d(x,y) from y.
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.Evaluation of Noncommutative Polynomials at Bounded Operators: a Unital Homomorphism Compatible with Adjoints, Substitution, Representations and the GNS Multiplication Operators
lemmalem:nc-polynomial-evaluation-operators-2026aAnalysisAlgebraEvaluation at a tuple of bounded operators is a unital algebra homomorphism that respects adjoints for self-adjoint tuples, commutes with substitution and with unital multiplicative linear maps, turns GNS left multiplications into L_p, and obeys the bound R^k on words of length k…Evaluation of Noncommutative Polynomials at a Tuple of Bounded Operators
definitiondef:nc-polynomial-evaluation-operators-2026aAnalysisAlgebraDefines the value p(T) of a noncommutative polynomial at a tuple T of bounded operators on a complex Hilbert space, sending each monomial to the product of the operators along its word.Linear Maps from Noncommutative Polynomials into Bounded Operators: Existence and Uniqueness from Values on Monomials
lemmalem:nc-operator-linear-extension-2026aAnalysisAlgebraAny assignment of bounded operators to words extends uniquely to a linear map from noncommutative polynomials into bounded operators, given by summing over the support of a polynomial in any order.The Amalgamated Free Product of Two Noncommutative Laws over a Common Marginal: Representations, Amalgamation, Freeness and the Tracial Vacuum State
theoremthm:nc-amalgamated-free-product-2026aAnalysisAlgebraThe two tracial algebras act on the amalgamated free product space by unital *-representations that agree on the marginal algebra, alternating products of centred elements applied to the vacuum give the tuple vectors, the vacuum state restricts to the given traces, and it is inva…Cyclic Symmetry of Nested Conditional Expectations over a Common Marginal
lemmalem:nc-nested-expectation-cyclic-2026aAnalysisAlgebraA nested conditional expectation folded from the inside out and the same expression folded from the outside in have the same trace against given elements of the marginal algebra.The Amalgamated Free Product Space: Multilinearity of the Tuple Vectors and the Bounded Left Actions of the Two Tracial Algebras
lemmalem:nc-free-product-actions-2026aAnalysisAlgebraIn the amalgamated free product space the tuple vectors are multilinear and balanced over the marginal algebra, the formal actions are linear, unital and multiplicative up to null vectors and agree on the marginal algebra, and each extends to a bounded operator of norm at most th…The Amalgamated Free Product Space of Two Noncommutative Laws over a Common Marginal, Its Vacuum Vector and Vacuum State
definitiondef:nc-free-product-space-2026aAnalysisAlgebraDefines the amalgamated free product space of two noncommutative laws over a common marginal as the Hilbert completion of the formal space, with its tuple vectors, vacuum vector and vacuum state.The Formal Amalgamated Free Product: the Free Vector Space, Positivity of the Nested-Expectation Form, and Linearity and Formal Adjoints of the Actions
lemmalem:nc-free-product-formal-2026aAnalysisAlgebraThe formal free product space is a complex vector space, the nested-expectation form is Hermitian and positive semidefinite (via positive Gram operators and their square roots), and the formal actions are linear with formal adjoints.The Formal Amalgamated Free Product over a Common Marginal: Alternating Tuples, the Free Vector Space, the Nested-Expectation Form and the Formal Actions
definitiondef:nc-free-product-formal-2026aAnalysisAlgebraDefines the formal amalgamated free product of two tracial algebras over the tracial algebra of a common marginal: centred parts, alternating tuples of centred elements, the free vector space on them and on the marginal algebra, the nested-expectation form, and the formal left ac…Two Noncommutative Laws with a Common Marginal: Standing Notation for Their Amalgamated Free Product
settingset:nc-amalgamation-2026aAnalysisAlgebraStanding notation for two noncommutative laws with a common marginal: their tracial algebras, the tracial algebra of the marginal, the embeddings and the conditional expectations.Marginals of a Noncommutative Law: the Isometry of GNS Spaces, the Trace-Preserving Embedding of Tracial Algebras and the Conditional Expectation
lemmalem:marginal-embedding-nc-law-2026aAnalysisFor a law and a tuple of self-adjoint polynomials, the pulled-back law is a law; the substitution induces an isometry between the complex GNS spaces; its tracial algebra embeds into that of the original law by a unital, injective, trace-preserving *-homomorphism; and compression…The Tracial Algebra of a Noncommutative Law: a Norm-Closed Unital *-Algebra with a Faithful Positive Trace, Determined by Vacuum Vectors, Closed under Square Roots
lemmalem:tracial-algebra-basic-nc-law-2026aAnalysisThe tracial algebra of a law contains the left multiplications and is closed under the algebra operations, adjoints and norm limits; its elements are determined by their value at the vacuum, which characterises them as the bounded vectors; the vacuum expectation is a faithful pos…The Tracial Algebra of a Noncommutative Law and Its Trace
definitiondef:tracial-algebra-nc-law-2026aAnalysisThe tracial algebra of a noncommutative law is the set of bounded operators on its complex GNS space that commute with every right multiplication by a polynomial; its trace is the vacuum expectation.Left and Right Multiplication Operators on the Complex GNS Space of a Noncommutative Law: Boundedness, Algebra Rules, Adjoints, Commutation, the Vacuum and the Conjugation
lemmalem:gns-operators-nc-law-2026aAnalysisFor a noncommutative law, left and right multiplication by a polynomial extend to bounded operators on the complex GNS space; left multiplication is a homomorphism and right multiplication an antihomomorphism, adjoints correspond to polynomial adjoints, left and right multiplicat…The Complex GNS Space of a Tracial State on Noncommutative Polynomials
definitiondef:complex-gns-space-nc-law-2026bAnalysisThe complex GNS space of a tracial state on noncommutative polynomials is the complex Hilbert completion of the polynomials under the form sending (p, q) to the state of p* q; it comes with the classes of polynomials and the vacuum vector, the class of the unit.