Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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 the GNS space of a noncommutative law as the real Hilbert completion of the self-adjoint polynomials under the pairing given by the law.
The Hilbert Completion is a Real Hilbert Space Containing a Dense Isometric Image, and Bounded Linear Maps Extend to It
theoremthm:hilbert-completion-semi-inner-product-2026aAnalysisThe Hilbert completion is a real Hilbert space into which the original space maps isometrically with dense image, and bounded linear maps extend uniquely to it.The Hilbert Completion of a Real Vector Space with a Positive Semidefinite Symmetric Bilinear Form
definitiondef:hilbert-completion-semi-inner-product-2026aAnalysisDefines the Hilbert completion of a real vector space with a positive semidefinite symmetric bilinear form, as cosets of Cauchy sequences modulo null sequences, with its canonical map.Cauchy Sequences for a Positive Semidefinite Symmetric Bilinear Form: Cauchy-Schwarz, the Space of Cauchy Sequences, Convergence of Pairings, and Null Sequences
lemmalem:semi-inner-product-cauchy-sequences-2026aAnalysisFor a positive semidefinite symmetric bilinear form: Cauchy-Schwarz, the vector space of Cauchy sequences, convergence of pairings, null sequences and their cosets.Cesaro Means of a Convergent Real Sequence Converge to Its Limit
lemmalem:cesaro-mean-real-2026bAnalysisIf a sequence of real numbers converges to a, then the averages of its first m terms converge to a as well.Basic Properties of the Legendre-Fenchel Conjugate: the Fenchel-Young Inequality, Convexity, Full Domain under Superlinear Growth, and the Quadratic
lemmalem:legendre-fenchel-conjugate-basic-rn-2026aAnalysisThe conjugate satisfies the Fenchel-Young inequality, has a convex domain on which it is convex whatever f is, is defined everywhere when f grows faster than every linear function, and maps half the squared norm to itself.The Legendre-Fenchel Conjugate of a Real Function on a Subset of Euclidean Space
definitiondef:legendre-fenchel-conjugate-rn-2026aAnalysisFor a real function f on a nonempty subset C of Euclidean space, the conjugate is defined at every p for which p.x - f(x) is bounded above on C, and there equals its supremum.Sequential Banach-Alaoglu Theorem: Bounded Sequences in the Dual of a Separable Real Normed Space Have Weak-Star Convergent Subsequences
theoremthm:banach-alaoglu-sequential-2026aAnalysisIn the dual of a separable real normed space, every sequence bounded in the dual norm by M has a subsequence converging weak-star to a functional of dual norm at most M.The Dual of a Real Normed Space is a Real Banach Space, and the Dual Norm is the Least Bound
lemmalem:dual-space-basic-2026aAnalysisThe bounded linear functionals on a real normed space form a real vector space under pointwise operations; the dual norm is the least nonnegative bound of a functional, is a norm, and makes the dual a Banach space. Weak-star limits are unique, and norm convergence implies weak-st…Weak-Star Convergence in the Dual of a Real Normed Space
definitiondef:weak-star-convergence-dual-2026aAnalysisA sequence of bounded linear functionals on a real normed space converges weak-star to a bounded linear functional when it converges to it at every vector.The Dual Space of a Real Normed Space and the Dual Norm
definitiondef:dual-space-real-normed-2026aAnalysisThe dual of a real normed space is the set of bounded linear functionals on it, with pointwise addition and scalar multiplication, and the dual norm of a functional is the greatest lower bound of its nonnegative bounds.Mean-Field Limit of the N-Particle Dyson Game: the Value per Particle Converges to the Solution of the Dyson Hamilton-Jacobi Equation on the Wasserstein Space
theoremthm:dyson-n-particle-mean-field-limit-2026aAnalysisProbabilityPDEFor N particles on the line with logarithmic repulsion beta/(2(N-1)), a confining potential, idiosyncratic noise sigma^2/(N-1) below the collision threshold sigma^2 < beta and mean-field running cost, the solution of the N-particle Hamilton-Jacobi equation divided by N converges,…