Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Elementary Properties of Weak Convergence in a Real Inner Product Space
lemmalem:weak-convergence-basic-2026aAnalysisWeak limits are unique; strong convergence implies weak convergence; weak limits respect sums, multiples and subsequences; a norm bound on a weakly convergent sequence passes to the limit; weak convergence plus convergence of norms gives strong convergence (Radon-Riesz); bounded…Weak Convergence of a Sequence in a Real Inner Product Space
definitiondef:weak-convergence-hilbert-2026aAnalysisA sequence converges weakly to x if its inner products against every fixed vector converge to those of x.Exhausting Sequences of Finite-Dimensional Subspaces in a Separable Real Hilbert Space, and Their Projections
lemmalem:exhausting-subspaces-separable-hilbert-2026aAnalysisA separable real Hilbert space has a nondecreasing sequence of finite-dimensional closed subspaces with dense union; for any such sequence the orthogonal projections P_n converge pointwise to the identity, the tails Q_n = id - P_n decrease in norm to zero, and Q_n x_n -> 0 along…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…The Riesz Representation Theorem for a Real Hilbert Space
theoremthm:riesz-representation-hilbert-2026aAnalysisEvery bounded linear functional on a real Hilbert space is of the form x -> <x,z> for a unique z, and the norm of the functional equals |z|.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.Nearest-Point Projection onto a Nonempty Closed Convex Subset of a Real Hilbert Space
theoremthm:projection-closed-convex-hilbert-2026aAnalysisEvery point of a real Hilbert space has a unique nearest point in a nonempty closed convex set, characterised by a variational inequality; the projection is nonexpansive.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.- A real inner product space is a real Hilbert space if, with its induced norm, it is a real Banach space.
The Norm Metric of a Real Inner Product Space: Triangle Inequalities, Limits and Continuity
lemmalem:real-inner-product-metric-2026aAnalysisThe triangle and reverse triangle inequalities, that d(x,y)=|x-y| is a metric, the algebra of limits, sequential continuity of the inner product and norm, the description of bounded sets, and Lipschitz continuity of the norm and of the maps x -> <x,z>.The Cauchy–Schwarz Inequality in a Real Inner Product Space
theoremthm:cauchy-schwarz-real-2026bAnalysisLinear AlgebraIn a real inner product space the absolute value of the inner product of two vectors is at most the product of their norms.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.- An inner product on a real vector space is a symmetric function to the reals, linear in the first argument and positive definite; a real inner product space carries one, and its induced norm is the square root of the inner product of a vector with itself.