Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Properties of the Product of Two Real Inner Product Spaces
lemmalem:product-inner-product-space-2026aAnalysisThe norm of a pair, the comparison with the product metric, componentwise convergence and the Cauchy condition, boundedness of the coordinate maps and injections, and the inheritance of completeness and separability.- The Cartesian product of two real inner product spaces, equipped with componentwise addition and scalar multiplication and with the pairing given by the sum of the two inner products, together with its coordinate maps and injections.
Elementary Properties of Series in a Real Inner Product Space
lemmalem:series-inner-product-space-2026aAnalysisLinearity, vanishing of the terms, telescoping, the Cauchy criterion and absolute convergence in a Hilbert space, the behaviour of a series under a bounded linear map and under the inner product, and agreement with series of real numbers.- Partial sums of a sequence of vectors, convergence of the associated series in the metric of the space and its sum, and absolute convergence.
Functions with Closed Superlevel Sets: Sequential Characterisation, Semicontinuity, Perturbation and Limits
lemmalem:closed-superlevel-basic-2026aAnalysisHaving closed superlevel sets in the ambient space is characterised by a sequential condition, implies upper semicontinuity, is preserved by subtracting a continuous function, and forces the limit of a convergent sequence of values to be dominated by the value at the limit point.Elementary Properties of Sequentially Strict Extrema
lemmalem:sequentially-strict-extremum-basic-2026aAnalysisA sequentially strict maximum is a strict maximum and is attained at only one point; the notion passes to negatives, to affine changes of the function, to the addition of a function already maximised at the same point, and to restriction.Series of Nonnegative Real Numbers, Comparison, and the Geometric Series
lemmalem:series-real-nonnegative-2026aAnalysisA series with nonnegative terms converges exactly when its partial sums are bounded above, and its sum is then their supremum; the comparison test; and the geometric series with its tails.- 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 and finite sums, sequences and their limits, and suprema and infima, together with the elementary arithmetic and limit 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-2026aAnalysisDefines 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-2026aAnalysisAlong 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-2026aAnalysisAn 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-2026aAnalysisEvery 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-2026aAnalysisConstant 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-2026aAnalysisA 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-2026aAnalysisDefines 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-2026aAnalysisDefines 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.