Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.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.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.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.- The map sending an index a of the initial segment [N] to N+1-a is a bijection of [N] onto itself, and a finite sum is unchanged when its summands are taken in reverse order.
The Expansion of the Square and the Fourth Power of a Sum of Real Numbers
lemmalem:fourth-power-binomial-real-2026aAnalysisAlgebraThe square of a sum of two real numbers expands as the usual three terms, and the fourth power as the five terms with coefficients one, four, six, four and one.Constants, Powers, Sums, Scalar Multiples and Products of Polynomial Functions
lemmalem:polynomial-function-algebra-2026aAlgebraLet be a field, with additive identity and multiplicative identity , and let be the set of natural numbers. Let be polynomial functions on and let . Write , and for the pointwise sum, scalar multiple and…- Let be a field. A map is a polynomial function on if there are a natural number , an element , and a map on the initial segment determined by , with values written , such that…