Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Hilbert Triple: a Densely and Continuously Embedded Hilbert Space and Its Form Operator
definitiondef:hilbert-triple-2026aAnalysisPDEA Hilbert triple (H,V,A) consists of separable real Hilbert spaces V inside H, V dense in H with |x|_H <= |x|_V, and the operator A defined on the set D(A) of x in V whose V-inner product against V is represented by an element Ax of H.Bounded Sequences in a Separable Real Hilbert Space Have Weakly Convergent Subsequences
theoremthm:weak-sequential-compactness-separable-hilbert-2026aAnalysisEvery sequence bounded by R in a separable real Hilbert space has a subsequence converging weakly to a limit of norm at most R.The Diagonal Subsequence Lemma for Bounded Real Arrays
lemmalem:diagonal-subsequence-real-2026bAnalysisFor a doubly indexed array of real numbers whose columns are bounded sequences, a single strictly increasing sequence of row indices makes every column converge.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 Hilbert space is a real inner product space that is complete for its norm metric; fixes the topological vocabulary (open, closed, dense, bounded, convergent, Cauchy) used for inner product spaces and the notion of closed linear subspace.
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>.