Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Vanishing of Uniformly Small Linear, Quadratic and Bilinear Terms in a Real Inner Product Space
lemmalem:small-terms-vanish-hilbert-2026aAnalysisA vector, or a bounded symmetric bilinear form, whose associated linear, quadratic or bilinear expression is bounded by an arbitrarily small multiple of the corresponding power of the norm on some ball, vanishes identically. These are the uniqueness statements behind the gradient…Exhausting Sequence of Finite-Dimensional Subspaces of a Real Hilbert Space
definitiondef:exhausting-sequence-hilbert-2026aAnalysisA nondecreasing sequence of finite-dimensional closed linear subspaces whose union is dense.- Standing notation for work on a Hilbert triple (H,V,A): the two spaces with subscripted notation, separability of V as a standing hypothesis, the form operator, Riesz map and resolvents, the penalty function h = (1/2)|x|_V^2, the traces V∩U and W = D(A)∩U of an open set U with th…
- Standing notation for real Hilbert spaces: numbers and sequences by reference to the real-numbers setting, the space, topology (including restricted metrics on subsets), bounded linear maps, bounded symmetric bilinear forms, projections, weak convergence, separability and exhaust…
Weak Compactness and Closedness of Bounded Subsets of the Small Space of a Hilbert Triple
lemmalem:hilbert-triple-closure-2026aAnalysisPDEIn a Hilbert triple (H,V,A), a V-bounded sequence has a subsequence converging weakly in V and in H to a point of V with the same norm bound; a V-bounded sequence converging in H has its limit in V with |x|_V <= R.The Resolvent of the Form Operator of a Hilbert Triple: Minimisation, Contraction, and Density of the Domain
theoremthm:hilbert-triple-resolvent-2026aAnalysisPDEFor alpha > 0 and x-bar in H the functional (1/2)|x|_V^2 + alpha |x - x-bar|_H^2 has a unique minimiser R_alpha x-bar on V, which lies in D(A) and solves A x + 2 alpha x = 2 alpha x-bar; R_alpha is an H-contraction, R_alpha x-bar -> x-bar in H as alpha -> infinity, and D(A) is de…Elementary Properties of a Hilbert Triple: the Embedding, the Riesz Map and the Form Operator
lemmalem:hilbert-triple-basic-2026aAnalysisPDEIn a Hilbert triple the inclusion V -> H is a bounded linear map carrying convergence and weak convergence from V to H; the Riesz map J: H -> V representing <z,.>_H on V is linear, injective and nonexpansive; D(A) is the range of J, A is linear and symmetric, and <Ax,x>_H = |x|_V…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-2026aAnalysisGiven real numbers a_{m,k} bounded in m for each fixed k, one strictly increasing index sequence 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…