TheoremBase

Theorems

A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.

Showing 41-60 of 123
  • Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space with zero vector 0V0_{V}, and let TT be a linear operator on VV that is self-adjoint and positive semi-definite. Let z|z| denote the modulus of a complex number zz. Then the following hold.…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let KK be a field, let VV be a vector space over KK with zero vector 0V0_{V}, and let WW be a linear subspace of VV. Then the following hold. 1. (Vector space) The set WW, equipped with the restrictions to WW of the addition and the scalar multiplication of VV, is a vect…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let KK be a field, let VV be a vector space over KK, let nn be a natural number, let [n][n] be the initial segment determined by nn, let vVnv\in V^{n} be an nn-tuple in VV with components vkv_{k}, and let span(v)\operatorname{span}(v) be its span. Then the following hold.…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Finite-Dimensional Vector Space

    definitiondef:finite-dimensional-vector-space-2026bAlgebraLinear Algebra
    Let KK be a field and let VV be a vector space over KK with zero vector 0V0_{V}. The space VV is finite-dimensional if V={0V}V=\{0_{V}\}, or if there exist a natural number nn and an nn-tuple eVne\in V^{n} that is a basis of VV.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Span of a Finite Family of Vectors

    definitiondef:span-finite-family-2026bAlgebraLinear Algebra
    Let KK be a field, let VV be a vector space over KK, let nn be a natural number, and let vVnv\in V^{n} be an nn-tuple in VV, with components vkv_{k}. The span of vv is the set…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space with zero vector 0V0_{V} and induced norm \lVert\cdot\rVert, and let dd be the map with d(u,v)=uvd(u,v)=\lVert u-v\rVert, which is a metric on VV by claim 3 of…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space that has an orthonormal basis eVne\in V^{n} for some natural number nn, where VnV^{n} is the set of nn-tuples in VV. By Uniqueness of the Adjoint, and Existence in Finite Dimensions every…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space with induced norm \lVert\cdot\rVert, which is a norm on VV by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let nn be a natural number, let eVne\in V^{n} be an nn-tuple in VV th…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Properties of the Operator Norm

    lemmalem:operator-norm-properties-2026aAnalysisLinear Algebra
    Let VV be a complex vector space equipped with a norm \lVert\cdot\rVert, let SS and TT be bounded linear operators on VV, and let λ\lambda be a complex number with modulus λ|\lambda|. Write Sop\lVert S\rVert_{\mathrm{op}} and Top\lVert T\rVert_{\mathrm{op}} for their…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Operator Norm

    definitiondef:operator-norm-2026aAnalysisLinear Algebra
    Let VV be a complex vector space equipped with a norm \lVert\cdot\rVert, let TT be a bounded linear operator on VV, and let cc be a real number. The number cc is an operator norm of TT if cc is a bound for TT and cCfor every bound C for T,c\le C\qquad\text{for every bound }C\text{ for }T,

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Existence and Uniqueness of the Operator Norm

    lemmalem:operator-norm-existence-uniqueness-2026aAnalysisLinear Algebra
    Let VV be a complex vector space equipped with a norm \lVert\cdot\rVert, and let TT be a bounded linear operator on VV. Let BTB_{T} denote the set of those real numbers that are of the form T(u)\lVert T(u)\rVert for some uVu\in V with u1\lVert u\rVert\le1, the order being that…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let VV be a complex vector space equipped with a norm \lVert\cdot\rVert, let TT be a linear operator on VV, and let CC be a real number with 0C0\le C, the order being that of the ordered field of real numbers. The number CC is a bound for TT if…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Let VV be a complex vector space equipped with a norm \lVert\cdot\rVert, let nn be a natural number, let [n][n] be the initial segment determined by nn, and let v:[n]Vv:[n]\to V be a map with values vkv_{k}. Then…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Positive Definite Operator

    definitiondef:positive-definite-operator-2026aAnalysisLinear Algebra
    Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space with zero vector 0V0_{V}, and let TT be a linear operator on VV. The operator TT is positive definite if for every uVu\in V the complex number u,T(u)\langle u,T(u)\rangle is a real number satisfyin…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Properties of Unitary Operators

    lemmalem:unitary-preserves-inner-product-2026bAnalysisLinear Algebra
    Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space, with induced norm \lVert\cdot\rVert, which is a norm on VV by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let TT be a unitary operator on VV. Throughout, \lVert\cdot\rVert

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Orthogonal Projection

    definitiondef:orthogonal-projection-2026bAnalysisLinear Algebra
    Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space, let PP be a linear operator on VV, and let the product of operators be as in that definition. The operator PP is an orthogonal projection if it is self-adjoint and satisfies PP=P.PP=P.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Positive Semi-Definite Operator

    definitiondef:positive-semidefinite-operator-2026aAnalysisLinear Algebra
    Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space and let TT be a linear operator on VV. The operator TT is positive semi-definite if for every uVu\in V the complex number u,T(u)\langle u,T(u)\rangle is a real number satisfying…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Unitary Operator

    definitiondef:unitary-operator-2026bAnalysisLinear Algebra
    Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space and let TT be a linear operator on VV. The operator TT is unitary if it is surjective, that is, every vVv\in V satisfies v=T(u)v=T(u) for some uVu\in V, and if…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Self-Adjoint Operator

    definitiondef:self-adjoint-operator-2026bAnalysisLinear Algebra
    Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space and let TT be a linear operator on VV. The operator TT is self-adjoint if T(u),v=u,T(v)for all u,vV.\langle T(u),v\rangle=\langle u,T(v)\rangle\qquad\text{for all }u,v\in V.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Let VV together with ,\langle\cdot,\cdot\rangle be a complex inner product space that has an orthonormal basis eVne\in V^{n} for some natural number nn, where VnV^{n} is the set of nn-tuples in VV. By Uniqueness of the Adjoint, and Existence in Finite Dimensions every…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

Showing 41-60 of 123