Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Plan Jets and Hamiltonians on Square-Integrable Noncommutative Laws: Standing Notation
settingset:nc-plan-jets-2026aAnalysisPDEStanding notation for plan jets and Hamiltonians on square-integrable noncommutative laws: tuple sums and pairing, lifts of functions on laws to tuples, and the metrics used.Tracial W*-Probability Spaces and Square-Integrable Tuples: Standing Notation
settingset:tracial-w-star-l2-2026aAnalysisProbabilityStanding notation for tracial W*-probability spaces, their traces, conjugations and self-adjoint vectors, trace-preserving embeddings, self-adjoint and L^2 tuples and their laws, with the basic results on them in force.Every Square-Integrable Noncommutative Law is the Law of a Square-Integrable Tuple; Realisation of Couplings and of Almost Optimal Pairs
theoremthm:l2-law-realisation-2026aAnalysisProbabilityEvery L^2 noncommutative law is the law of an L^2 tuple in some tracial W*-probability space; likewise every L^2 law of 2d variables is the law of a pair of L^2 tuples, and any two L^2 laws are the laws of two tuples in a common space whose squared L^2 distance is within any marg…Gluing a Chain of Noncommutative Couplings into Consistent Joint Laws
lemmalem:nc-chain-gluing-2026aAnalysisProbabilityGiven a sequence of noncommutative laws and couplings between consecutive terms, there is a consistent sequence of joint laws of the first k blocks of variables whose consecutive pairs of blocks have the given couplings as laws.Calculus of Laws of Square-Integrable Tuples: Bounded Tuples, the Lipschitz Bound, Moments, Affine Push-Forwards, Couplings and Embeddings
lemmalem:l2-tuple-law-properties-2026aAnalysisProbabilityThe law of an L^2 tuple extends the law of bounded self-adjoint tuples, is 1-Lipschitz for the L^2 norm, has its moments given by inner products, commutes with affine push-forwards, turns pairs into L^2 couplings whose cost is the squared L^2 distance, and is invariant under trac…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.Inductive Limits of Tracial W*-Probability Spaces along Trace-Preserving Embeddings
theoremthm:inductive-limit-tracial-w-star-2026aAnalysisA sequence of tracial W*-probability spaces linked by trace-preserving embeddings has an inductive limit: a tracial W*-probability space receiving compatible trace-preserving embeddings of every term, whose images are dense and generate it as a double commutant.Trace-Preserving Embeddings Preserve Operator Norms and Compose
lemmalem:trace-preserving-embedding-basic-2026aAnalysisA trace-preserving embedding of tracial W*-probability spaces preserves operator norms, and the composite of two such embeddings is again one, implemented by the composite isometry.The Conditional Expectation of a Trace-Preserving Embedding: Values in the Subalgebra, Bimodule Property, Trace, Positivity, Contraction and the Jones Projection
lemmalem:conditional-expectation-tracial-2026aAnalysisThe conditional expectation of a trace-preserving embedding takes values in the smaller algebra, is a positive, contractive, trace-preserving bimodule map that is a left inverse of the embedding, and acts on vectors through the orthogonal projection onto the closure of the embedd…Trace-Preserving Embeddings of Tracial W*-Probability Spaces, Their Implementing Isometries and Conditional Expectations
definitiondef:trace-preserving-embedding-2026aAnalysisA trace-preserving embedding is a trace-preserving unital -homomorphism between tracial W-probability spaces; its implementing isometry V gives the conditional expectation b maps to V* b V.A Trace-Preserving Unital -Homomorphism between Tracial W-Probability Spaces is Implemented by an Isometry
lemmalem:trace-preserving-homomorphism-isometry-2026aAnalysisA trace-preserving unital -homomorphism between tracial W-probability spaces is injective and is implemented by a unique isometry between the Hilbert spaces that maps the cyclic vector to the cyclic vector and intertwines the homomorphism and the conjugations.The Tracial Algebra of a Noncommutative Law is a Tracial W*-Probability Space: the W*-Closure of the Left Multiplications
lemmalem:nc-law-tracial-w-star-2026aAnalysisFor a noncommutative law, the left multiplication operators with the vacuum form a cyclic tracial operator algebra whose conjugation is the GNS conjugation and whose W*-closure is the tracial algebra of the law; the variables realise the law in the vacuum state.Standard Form of a Tracial W*-Probability Space: the Commutation Theorem, Right-Bounded Vectors, Faithfulness and Self-Adjoint Vectors
theoremthm:tracial-w-star-standard-form-2026aAnalysisIn a tracial W*-probability space the commutant is the conjugate of the algebra, right-bounded vectors come from elements of the algebra, the trace is faithful, and the conjugation-fixed vectors form a real Hilbert space in which the vectors of self-adjoint elements are dense.The Tracial W*-Closure of a Cyclic Tracial Operator Algebra: the Commutant of the Right Action is a Tracial W*-Probability Space Equal to the Double Commutant
theoremthm:tracial-w-star-closure-2026aAnalysisThe commutant of the right action of a cyclic tracial operator algebra contains the algebra, is a tracial W*-probability space for the same vector, equals the double commutant of the algebra, has commutant equal to its own conjugate, and contains an element with any prescribed ri…The Trace, the Conjugation and the Right Action of a Cyclic Tracial Operator Algebra
lemmalem:cyclic-tracial-conjugation-2026aAnalysisThe trace of a cyclic tracial operator algebra is a faithful tracial state, the cyclic vector separates the algebra and its commutant, the map sending S Omega to S* Omega extends to a conjugation, and conjugating the algebra by it gives right multiplications, which lie in the com…- A tracial W*-probability space is a cyclic tracial operator algebra whose algebra equals its double commutant.
Cyclic Tracial Operator Algebras and Their Traces
definitiondef:cyclic-tracial-operator-algebra-2026aAnalysisA cyclic tracial operator algebra is a unital *-algebra of bounded operators on a complex Hilbert space together with a cyclic unit vector whose vector state is tracial on the algebra; that vector state is its trace.Basic Properties of Commutants: Unital Algebras Closed under Weak Limits, Order Reversal, the Triple Commutant, and Conjugation
lemmalem:commutant-basic-2026aAnalysisCommutants are unital algebras closed under weak operator limits and under adjoints when the set is; taking commutants reverses inclusions, a set lies in its double commutant and the triple commutant equals the commutant; conjugation by a conjugation commutes with taking commutan…