Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Linearity, vanishing of the terms, the Cauchy criterion, comparison of sums, the relation between a series and its tails, and telescoping series.
A Real Function with Closed Superlevel Sets on a Subset of a Metric Space
definitiondef:closed-superlevel-sets-2026aAnalysisThe superlevel sets of a real function defined on a subset of a metric space, and the condition that each of them be closed in the ambient space.Sequentially Strict Maxima and Minima on a Subset of a Metric Space
definitiondef:sequentially-strict-extremum-2026aAnalysisA maximum (or minimum) point at which every maximising (minimising) sequence converges to the point itself, the substitute for a strict extremum when bounded closed sets need not be compact.- Partial sums of a sequence of real numbers, convergence of the associated series and its sum, and absolute convergence.
- Standing notation for the real numbers, natural numbers, numerals, integers, finite sums, sequences and bounds, with the elementary arithmetic, order, counting and finite-sum results in force by reference.
The Second Derivative and the Hessian on an Open Subset of a Real Inner Product Space
definitiondef:second-derivative-hilbert-2026bAnalysisDefines the second derivative of a real-valued function at a point of an open subset of a real inner product space as a bounded symmetric bilinear form giving a uniform first-order expansion of the gradient near that point, and defines that form as the Hessian.Segment Derivatives, the Second-Order Taylor Expansion, and the Second-Order Condition at a Local Extremum
lemmalem:taylor-c2-hilbert-2026bAnalysisAlong a segment a differentiable function has one-dimensional derivative the inner product of its gradient with the direction; a function with a second derivative at a point admits the second-order Taylor expansion there; and at a local maximum its gradient vanishes and its Hessi…Affine and Quadratic Functions on a Real Hilbert Space are of Class
lemmalem:quadratic-c2-hilbert-2026bAnalysisAn affine function, half a bounded symmetric bilinear form evaluated on the diagonal, and a multiple of the squared distance to a fixed point are of class on a real Hilbert space, with gradients and Hessians computed explicitly, and remain so on any open subset.The Bounded Symmetric Operator Represented by a Bounded Symmetric Bilinear Form on a Real Hilbert Space
lemmalem:form-operator-hilbert-2026bAnalysisEvery bounded symmetric bilinear form on a real Hilbert space is the form of a unique bounded linear operator, which is symmetric and has the same norm; the correspondence is linear, carries the identity form to the identity map, and is inverted by taking the form of a symmetric…Constants, Sums, Scalar Multiples and Differences of Differentiable Functions on an Open Subset of a Real Inner Product Space
lemmalem:c2-algebra-hilbert-2026bAnalysisConstant functions are of class with vanishing gradient and Hessian, and differentiability, second derivatives and the classes and are preserved by sums, scalar multiples and differences, the gradient and the Hessian depending linearly on the function.Basic Properties of Differentiability on an Open Subset of a Real Inner Product Space
lemmalem:frechet-basic-hilbert-2026bAnalysisA function differentiable at a point satisfies a local Lipschitz bound there and is continuous there; its gradient vanishes at a local extremum; and differentiability, second derivatives and the classes and pass to smaller open sets without changing gradients or Hessi…The Classes and on an Open Subset of a Real Inner Product Space
definitiondef:c1-c2-hilbert-2026bAnalysisDefines the class on an open subset of a real inner product space by continuity of the gradient map, and the class by membership in together with the existence and continuity of the Hessian map.Fréchet Differentiability and the Gradient on an Open Subset of a Real Inner Product Space
definitiondef:frechet-differentiable-hilbert-2026bAnalysisDefines differentiability of a real-valued function at a point of an open subset of a real inner product space, with a first-order expansion whose linear part is an inner product against a vector, and defines that vector as the gradient.Vanishing of Uniformly Small Linear, Quadratic and Bilinear Terms in a Real Inner Product Space
lemmalem:small-terms-vanish-hilbert-2026bAnalysisA 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 a Hilbert triple: the two spaces and their subscripted notation, the standing separability hypothesis, the form operator with the Riesz and resolvent maps, the penalty function, open subsets of the larger space with their traces and the vocabulary used on th…
- Standing notation for real Hilbert spaces: numbers, maxima and minima, and sequences; the space; topology, including restricted metrics, balls, uniform continuity, moduli of continuity and restrictions of maps; bounded linear maps; bounded symmetric bilinear forms; projections; w…
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…