Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Cauchy-Schwarz Inequality for a Positive Semi-Definite Self-Adjoint Operator
lemmalem:positive-semidefinite-cauchy-schwarz-2026bAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and let be a linear operator on that is self-adjoint and positive semi-definite. Let denote the modulus of a complex number . Then the following hold.…A Linear Subspace is a Vector Space and Inherits an Inner Product
lemmalem:subspace-inner-product-space-2026bAnalysisAlgebraLinear AlgebraLet be a field, let be a vector space over with zero vector , and let be a linear subspace of . Then the following hold. 1. (Vector space) The set , equipped with the restrictions to of the addition and the scalar multiplication of , is a vect…The Span of a Finite Family is the Smallest Subspace Containing It
lemmalem:span-is-subspace-2026bAlgebraLinear AlgebraLet be a field, let be a vector space over , let be a natural number, let be the initial segment determined by , let be an -tuple in with components , and let be its span. Then the following hold.…Finite-Dimensional Vector Space
definitiondef:finite-dimensional-vector-space-2026bAlgebraLinear AlgebraLet be a field and let be a vector space over with zero vector . The space is finite-dimensional if , or if there exist a natural number and an -tuple that is a basis of .- Let be a field, let be a vector space over , let be a natural number, and let be an -tuple in , with components . The span of is the set…
Coordinate Isometry Determined by a Finite Orthonormal Basis
lemmalem:coordinate-isometry-orthonormal-basis-2026cAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector and induced norm , and let be the map with , which is a metric on by claim 3 of…Self-Adjointness, Unitarity and Orthogonal Projections Through the Adjoint in Finite Dimensions
lemmalem:operator-classes-via-adjoint-2026dAnalysisLinear AlgebraLet together with be a complex inner product space that has an orthonormal basis for some natural number , where is the set of -tuples in . By Uniqueness of the Adjoint, and Existence in Finite Dimensions every…Every Linear Operator on a Space with a Finite Orthonormal Basis is Bounded
lemmalem:finite-orthonormal-basis-operator-bounded-2026bAnalysisLinear AlgebraLet together with be a complex inner product space with induced norm , which is a norm on by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let be a natural number, let be an -tuple in th…- Let be a complex vector space equipped with a norm , let and be bounded linear operators on , and let be a complex number with modulus . Write and for their…
- Let be a complex vector space equipped with a norm , let be a bounded linear operator on , and let be a real number. The number is an operator norm of if is a bound for and …
Existence and Uniqueness of the Operator Norm
lemmalem:operator-norm-existence-uniqueness-2026aAnalysisLinear AlgebraLet be a complex vector space equipped with a norm , and let be a bounded linear operator on . Let denote the set of those real numbers that are of the form for some with , the order being that…Bound for a Linear Operator and Bounded Linear Operator
definitiondef:bounded-linear-operator-2026aAnalysisLinear AlgebraLet be a complex vector space equipped with a norm , let be a linear operator on , and let be a real number with , the order being that of the ordered field of real numbers. The number is a bound for if…Triangle Inequality for Finite Sums of Vectors
lemmalem:finite-sum-norm-triangle-2026aAnalysisLinear AlgebraLet be a complex vector space equipped with a norm , let be a natural number, let be the initial segment determined by , and let be a map with values . Then…- Let together with be a complex inner product space with zero vector , and let be a linear operator on . The operator is positive definite if for every the complex number is a real number satisfyin…
- Let together with be a complex inner product space, with induced norm , which is a norm on by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let be a unitary operator on . Throughout, …
- Let together with be a complex inner product space, let be a linear operator on , and let the product of operators be as in that definition. The operator is an orthogonal projection if it is self-adjoint and satisfies
Positive Semi-Definite Operator
definitiondef:positive-semidefinite-operator-2026aAnalysisLinear AlgebraLet together with be a complex inner product space and let be a linear operator on . The operator is positive semi-definite if for every the complex number is a real number satisfying…- Let together with be a complex inner product space and let be a linear operator on . The operator is unitary if it is surjective, that is, every satisfies for some , and if…
- Let together with be a complex inner product space and let be a linear operator on . The operator is self-adjoint if
Algebraic Properties of the Adjoint in Finite Dimensions
lemmalem:adjoint-properties-2026cAnalysisLinear AlgebraLet together with be a complex inner product space that has an orthonormal basis for some natural number , where is the set of -tuples in . By Uniqueness of the Adjoint, and Existence in Finite Dimensions every…