Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Commutant of a Set of Bounded Operators on a Complex Hilbert Space
definitiondef:commutant-complex-hilbert-2026aAnalysisThe commutant of a set of bounded operators consists of the bounded operators commuting with each of them; the double and triple commutants are iterated commutants.- A conjugation of a complex Hilbert space is an additive, conjugate-homogeneous involution that reverses inner products; conjugating an operator by it gives the map J A J.
Bounded Linear and Conjugate-Linear Maps on a Dense Subspace of a Complex Hilbert Space Extend Uniquely
lemmalem:dense-subspace-extension-complex-hilbert-2026aAnalysisA bounded linear or conjugate-linear map on a dense linear subspace of a complex Hilbert space extends uniquely to a continuous map on the whole space with the same bound, isometries extending to isometries; bounded operators agreeing weakly on a dense subspace are equal.- Standing notation for L2 noncommutative laws: the completion and its metric, affine data and push-forwards, moments, couplings and cost, with the basic results in force.
The Distance between Square-Integrable Noncommutative Laws is the Infimum of the Cost over Their Couplings
theoremthm:nc-l2-wasserstein-couplings-2026aAnalysisAny two L2 laws have L2 couplings, and the squared completion distance between them equals the infimum of the cost over those couplings; almost optimal couplings are obtained by chain gluing of optimal couplings of bounded approximations.Calculus of Square-Integrable Noncommutative Laws: Agreement on Bounded Laws, Lipschitz Estimates, Functoriality of Push-Forwards, Moment Formulas, Positivity, the Cost and the Diagonal Coupling
lemmalem:nc-l2-laws-calculus-2026aAnalysisOn L2 laws, push-forwards and moments agree with the bounded ones, satisfy the same Lipschitz estimates, compose functorially and obey the same moment formulas and positivity; every joint law couples its marginals with cost at least the squared distance, and the diagonal coupling…Square-Integrable Noncommutative Laws: the Wasserstein Completion of the Laws, Affine Push-Forwards, Moments, Couplings and Cost
definitiondef:nc-l2-laws-2026aAnalysisThe L2 laws of d variables form the metric completion of the noncommutative laws under the Wasserstein distance; affine push-forwards and first and quadratic moments are defined on it by continuous extension, and couplings and their cost through the marginal and difference data.Wasserstein Estimates for Affine Push-Forwards, First and Quadratic Moments, and the Cost of a Joint Law
lemmalem:nc-affine-moments-wasserstein-2026aAnalysisAffine substitutions are Lipschitz for the noncommutative Wasserstein distance, first moments and the root second moment are 1-Lipschitz, quadratic moments are Lipschitz on bounded sets, so all of them preserve Cauchy sequences; the cost of a joint law dominates the squared dista…Affine Substitutions of Noncommutative Laws: Self-Adjointness, Composition, Moment Formulas and Positivity, and the Coordinate Data
lemmalem:nc-affine-substitution-basic-2026aAnalysisAffine substitutions map laws to laws and compose like the affine data; the first and quadratic moments of a law are real, symmetric and positive semidefinite, they transform by explicit formulas, and the coordinate data give the marginals, the diagonal and the cost.Affine Data and Affine Substitutions of Noncommutative Polynomials
definitiondef:nc-affine-substitution-2026aAnalysisAn affine datum is a real coefficient matrix with a real shift; it defines a tuple of self-adjoint polynomials of degree at most one, hence a substitution, together with a norm, composites, identities and the marginal, difference and diagonal data.The Metric Completion is a Complete Metric Space with a Dense Isometric Copy of the Space, and Maps Preserving Cauchy Sequences Extend to It
theoremthm:metric-completion-2026aAnalysisTopologyThe metric completion is a complete metric space into which the canonical map is an isometry with dense image; a map into a complete metric space that preserves Cauchy sequences extends uniquely, continuously and with the same Lipschitz constant.- The metric completion is the set of classes of Cauchy sequences under vanishing limit distance, with the limit distance, and the canonical map sends a point to the class of its constant sequence.
Cauchy Sequences in a Metric Space: Constant Sequences, Convergence of Termwise Distances, the Null Relation, and Independence of Representatives
lemmalem:cauchy-sequences-metric-2026aAnalysisTopologyFor Cauchy sequences in a metric space the termwise distances converge; the limit distance is a pseudometric, and vanishing limit distance is an equivalence relation compatible with it.Well-Posedness of the Eikonal and Discounted Hopf-Lax Equations on Noncommutative Laws with Distance Data
corollarycor:nc-eikonal-discounted-well-posed-2026aAnalysisPDEOn the space of noncommutative laws with a norm bound and the Wasserstein distance, the distance to a weak-star closed target set is the unique slope-based solution of the eikonal equation vanishing on the target, and a multiple of its square is the unique bounded solution of a d…The Noncommutative Laws with a Norm Bound Form a Complete Bounded Metric Space with Interpolation Points
theoremthm:nc-laws-complete-metric-2026aAnalysisProbabilityThe tracial states with norm bound R, with the noncommutative Wasserstein distance, form a complete and bounded metric space in which displacement interpolants are interpolation points.Moments of Noncommutative Laws are Lipschitz in the Wasserstein Distance
lemmalem:nc-moments-wasserstein-lipschitz-2026aAnalysisProbabilityOn laws with a norm bound, each moment is a Lipschitz function of the noncommutative Wasserstein distance; hence Wasserstein convergence implies weak-star convergence and sequentially weak-star closed sets are Wasserstein closed.Distance Functions Give Explicit Slope-Based Solutions of the Eikonal and Discounted Hopf-Lax Equations
propositionprop:distance-slope-solutions-metric-2026aAnalysisPDEIn a metric space with interpolation points, the distance to a nonempty set K solves the eikonal equation with right-hand side 1 off K, and a suitable multiple of its square solves the discounted Hopf-Lax equation with right-hand side a multiple of the squared distance.Comparison Principle for Slope-Based Solutions of the Discounted Hopf-Lax Equation on a Complete Metric Space with Interpolation Points
theoremthm:comparison-discounted-hopf-lax-metric-2026aAnalysisPDEOn a complete metric space with interpolation points, a bounded s-subsolution lies below a bounded s-supersolution of the discounted equation rho u + |grad u|^2/2 = f when f is uniformly continuous.Comparison Principle for Slope-Based Solutions of the Eikonal Equation on a Complete Metric Space with Interpolation Points
theoremthm:comparison-eikonal-metric-2026aAnalysisPDEOn a complete metric space with interpolation points, a bounded s-subsolution lies below a bounded s-supersolution of the eikonal equation off a set K, when the right-hand side is uniformly continuous and bounded below by a positive constant and the two are ordered uniformly near…The Discounted Stationary Hopf-Lax Equation on an Open Subset of a Metric Space
equationeq:discounted-hopf-lax-metric-2026aAnalysisPDENames the discounted stationary equation rho u + (1/2)|grad u|^2 = f on an open subset of a metric space, as the slope-based equation of the Hamiltonian rho r + p^2/2 - f(x).