Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.Definition of Sequences by Recursion on the Natural Numbers
lemmalem:sequence-recursion-natural-numbers-2026aSet TheoryGiven a starting point and a rule producing the next term from the index and the current term, there is exactly one sequence with that first term that obeys the rule.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.The Complex Hilbert Completion is a Complex Hilbert Space Containing a Dense Isometric Image, and Bounded Complex-Linear Maps Extend to It
theoremthm:hilbert-completion-complex-2026aAnalysisThe complex Hilbert completion of a positive semidefinite Hermitian form is a complex Hilbert space; the canonical map is complex-linear and carries the form to the inner product; its image is dense; and bounded complex-linear maps into a complex Hilbert space extend uniquely and…The Hilbert Completion of a Complex Vector Space with a Positive Semidefinite Hermitian Form
definitiondef:hilbert-completion-complex-2026aAnalysisDefines the complex Hilbert completion of a positive semidefinite Hermitian form: the real Hilbert completion of its real part, with multiplication by i extended by continuity and the complex inner product recovered from the real one.Square Roots of Positive Bounded Operators on a Complex Hilbert Space, Commuting with Everything that Commutes with the Operator
theoremthm:square-root-positive-operator-complex-hilbert-2026aAnalysisEvery bounded, self-adjoint, positive semi-definite operator on a complex Hilbert space is the square of a bounded, self-adjoint, positive semi-definite operator that commutes with every bounded operator commuting with the given one.Finite Direct Sums of a Complex Hilbert Space: the Hilbert Structure, Coordinate Inclusions, Block Entries of Bounded Operators and Commutation with Diagonal Operators
lemmalem:finite-direct-sum-complex-hilbert-2026aAnalysisThe m-tuples in a complex Hilbert space form a complex Hilbert space; bounded operators on it correspond to m-by-m matrices of bounded operators, with the usual rules for products and adjoints, and an operator commutes with a diagonal operator exactly when every entry commutes wi…Complex Hilbert Spaces and Bounded Linear Maps: Standing Notation
settingset:complex-hilbert-space-2026bAnalysisStanding notation for complex inner product spaces, complex Hilbert spaces and bounded linear maps between them: inner products linear in the second argument, induced norms, operator norms, adjoints, positivity, and the background results in force.Bounded Linear Maps between Complex Inner Product Spaces: the Least Bound, Operations, the Underlying Real Structure, Adjoints, Completeness and the Quadratic-Form Bound
lemmalem:bounded-maps-complex-inner-product-2026aAnalysisBasic facts on bounded linear maps between complex inner product spaces: the operator norm is the least bound, the algebraic operations, the real inner product given by the real part of a Hermitian form, existence and calculus of adjoints on Hilbert spaces, completeness of the sp…Adjoint of a Linear Map between Complex Inner Product Spaces
definitiondef:adjoint-linear-map-complex-2026aAnalysisA linear map S from W to V is an adjoint of a linear map T from V to W, between complex inner product spaces, when the inner product of Sw with v equals that of w with Tv.Bounded Linear Maps between Complex Normed Spaces and the Operator Norm
definitiondef:bounded-linear-map-complex-2026aAnalysisDefines bounded linear maps between two complex normed spaces, their bounds, the set of such maps, and the operator norm as the greatest lower bound of the bounds.- Defines positive semidefinite kernels on a finite set: Hermitian complex matrices indexed by the set whose quadratic forms are nonnegative.
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.