Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Defines positive semidefinite kernels on a finite set: Hermitian complex matrices indexed by the set whose quadratic forms are nonnegative.
Positive Semidefinite Kernels on a Finite Set: Rank-One Decomposition and the Schur Product
lemmalem:psd-kernel-finite-set-2026aLinear AlgebraSums of rank-one kernels are positive semidefinite, every positive semidefinite kernel on an N-element set is a sum of N rank-one kernels, and the entrywise (Schur) product of two positive semidefinite kernels is positive semidefinite.Lebesgue Measure under a Triangular or Symmetric Positive Definite Linear Map
lemmalem:lebesgue-linear-image-spd-2026aAnalysisLinear AlgebraLinear maps of Euclidean space are Borel, and Lebesgue integrals transform by the determinant under triangular matrices with positive diagonal and under symmetric positive definite matrices; in particular such a matrix multiplies Lebesgue measure by its determinant.Determinants of Positive Definite Matrices: Positivity, the Bound , Bounds under Pinching, and the Expansion of
lemmalem:log-determinant-bounds-2026aLinear AlgebraA symmetric positive definite d x d matrix A has positive determinant with log det A <= tr A - d. If epsilon I <= A <= L I, then A is positive definite and d - d/epsilon <= log det A <= dL - d. For a matrix B with entries bounded by m and |t| m small, det(I+tB) equals 1 + t tr B,…Compression of a Bounded Symmetric Bilinear Form along an Orthonormal Tuple
lemmalem:form-compression-hilbert-2026aAnalysisLinear AlgebraThe matrix of values of a bounded symmetric bilinear form on an orthonormal tuple is symmetric and its quadratic form is that of the original form along the span of the tuple; the compression is linear, does not increase the norm, preserves the order, sends the tail form to zero,…Coordinate Maps of a Finite Orthonormal Tuple: Forms, the Tail Form, and Quadratic Test Functions
lemmalem:coordinate-quadratic-hilbert-2026aAnalysisLinear AlgebraA finite orthonormal tuple in a Hilbert space gives a coordinate map onto Euclidean space; this lemma records its elementary properties, the bilinear forms and tail form it determines, and the fact that a Euclidean quadratic read through it is a twice continuously differentiable…The Real Vector Space of Real-Valued Functions on a Set
lemmalem:real-valued-function-space-2026aLinear AlgebraThe real-valued functions on any set form a real vector space under pointwise operations, and a subset containing the zero function and closed under those operations is a linear subspace.Projection onto the Span of an Orthonormal Tuple, and Coordinates on a Finite-Dimensional Subspace
lemmalem:finite-dimensional-subspace-hilbert-2026aAnalysisLinear AlgebraFor an orthonormal m-tuple e with span M, the map Px = sum <x,e_i> e_i is the orthogonal projection onto M: it is linear, idempotent, nonexpansive, satisfies Bessel's inequality and Pythagoras, M is closed, P x is the nearest point of M, and the coordinate map M -> R^m is a linea…Gram-Schmidt Orthonormalisation in a Real Inner Product Space
lemmalem:gram-schmidt-real-2026aAnalysisLinear AlgebraThe span of a finite tuple in a real inner product space is either the zero subspace or has an orthonormal basis of length at most that of the tuple; in particular every nonzero finite-dimensional subspace has an orthonormal basis.Inner Products Against Finite Sums, and Orthonormal Families, in a Real Inner Product Space
lemmalem:real-inner-product-finite-sums-2026aAnalysisLinear AlgebraThe inner product distributes over finite sums and linear combinations; for an orthonormal tuple the coefficients of a linear combination are recovered by pairing, its norm squared is the sum of squared coefficients, and the tuple is linearly independent.Elementary Properties of Bounded Symmetric Bilinear Forms: Norm, Quadratic Form, Order and Continuity
lemmalem:symmetric-bilinear-form-properties-2026aAnalysisLinear AlgebraSym(E) is a real vector space with a norm and metric; the norm is controlled by the quadratic form, so -cI <= b <= cI iff ||b|| <= c; the order is a partial order compatible with sums and nonnegative multiples; forms are continuous in all arguments; restriction to a subspace is o…Bounded Symmetric Bilinear Forms on a Real Inner Product Space: Norm, Order, Identity Form and Restriction
definitiondef:bounded-symmetric-bilinear-form-2026aAnalysisLinear AlgebraDefines the space Sym(E) of bounded symmetric bilinear forms on a real inner product space, its norm, the order b1 <= b2 given by comparing quadratic forms, the identity form I_E = <.,.> with its multiples cI, and the restriction of a form to a subspace carrying a stronger inner…Elementary Properties of Bounded Linear Maps and Functionals on Real Inner Product Spaces
lemmalem:bounded-linear-map-properties-2026aAnalysisLinear AlgebraThe operator norm bounds |Tx| by ||T|| |x| and is a supremum over the unit ball; boundedness is equivalent to Lipschitz continuity and to continuity; L(E,F) is a vector space with a norm; composition is submultiplicative; kernels are closed; and x -> <x,z> is a bounded functional…Bounded Linear Maps and Bounded Linear Functionals on Real Inner Product Spaces, and the Operator Norm
definitiondef:bounded-linear-map-inner-product-2026aAnalysisLinear AlgebraDefines bounded linear maps between real inner product spaces, the spaces L(E,F) and L(E), the operator norm as an infimum, and bounded linear functionals with their norm.Orthogonal Projection onto a Closed Linear Subspace of a Real Hilbert Space
corollarycor:orthogonal-projection-closed-subspace-2026aAnalysisLinear AlgebraFor a closed linear subspace M of a real Hilbert space, the nearest-point map P_M is linear and idempotent, characterised by x-P_M x being orthogonal to M, satisfies Pythagoras, and yields H = M + M^perp; a subspace is dense iff its orthogonal complement is trivial.Orthogonality, Orthogonal Complement and Orthonormal Families in a Real Inner Product Space
definitiondef:orthogonality-real-inner-product-2026aAnalysisLinear AlgebraDefines orthogonal vectors, the orthogonal complement of a subset, and orthonormal tuples and sequences in a real inner product space.Convex Subset of a Vector Space over the Real Numbers
definitiondef:convex-subset-real-vector-space-2026aAnalysisLinear AlgebraA subset of a real vector space is convex if it contains the segment tx+(1-t)y between any two of its points.The Cauchy-Schwarz Inequality in a Real Inner Product Space
theoremthm:cauchy-schwarz-real-2026aAnalysisLinear AlgebraIn a real inner product space, |<x,y>| is at most |x||y|.Elementary Identities in a Real Inner Product Space
lemmalem:real-inner-product-identities-2026aAnalysisLinear AlgebraBilinearity in the second argument, behaviour of the zero vector, vanishing and homogeneity of the norm, the expansions of |x±y|^2, the parallelogram law and the polarisation identity.- Defines real inner product spaces, the norm |x| as the nonnegative square root of <x,x>, and the distance d(x,y)=|x-y|.