Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
First- and Second-Order Conditions at a Local Extremum of a Function Penalised by on the Small Space
lemmalem:penalised-maximum-c2-hilbert-triple-2026aAnalysisPDEIf ψ is C^2 on an open subset U of H and ψ − λh has a local maximum on V∩U at x̂, then x̂ lies in D(A), λAx̂ = Dψ(x̂), and the restriction of D^2ψ(x̂) to V is at most λI_V; dually at a local minimum of ψ + λh.Viscosity Subsolution, Supersolution and Solution of a Second-Order Equation on a Hilbert Triple
definitiondef:viscosity-sub-supersolution-hilbert-triple-2026aAnalysisPDEA locally bounded above function u on an open subset U of the large space is a viscosity subsolution of F if, for every δ > 0, every C^2 test function φ and every local maximum x̂ of u^-_δ − φ on V∩U, the shifted operator F^-_δ can be made ≤ ε at data in W×R×H×Sym(H) within ε of…Classical Subsolution, Supersolution and Solution of a Second-Order Equation on a Hilbert Triple
definitiondef:classical-sub-supersolution-hilbert-triple-2026aAnalysisPDEA function of class C^2 on an open subset U of the large space is a classical subsolution of F if F(x, u(x), Du(x), D^2u(x)|_V) ≤ 0 at every point of W = D(A)∩U, a classical supersolution if the reverse inequality holds, and a classical solution if it is both.The -Envelopes and of a Function on an Open Subset of a Hilbert Triple
definitiondef:delta-envelopes-hilbert-triple-2026aAnalysisPDEFor a function u on an open subset U of the large space of a Hilbert triple, locally bounded above (below), and δ > 0, the δ-envelopes are u^-_δ = (u − δh)^* and u^+δ = (u + δh)*, the semicontinuous envelopes taken on V∩U for the metric of H.Degenerate Elliptic Second-Order Equation Operator on a Hilbert Triple
definitiondef:degenerate-elliptic-hilbert-triple-2026aAnalysisPDEA second-order equation operator on a Hilbert triple is degenerate elliptic if it is nonincreasing in its form argument for the order on bounded symmetric bilinear forms on V.Second-Order Equation Operator on an Open Subset of a Hilbert Triple and Its -Shifts
definitiondef:second-order-operator-hilbert-triple-2026aAnalysisPDEA second-order equation operator on an open set U of the large space of a Hilbert triple is a real function of (x, r, p, X) with x in W = D(A)∩U, r real, p in H and X a bounded symmetric bilinear form on V. Its δ-shifts feed F the penalised arguments r ± δh(x), p ± δAx and Y|_V ±…The Penalty Function of a Hilbert Triple: Expansion Identities, Closed Sublevel Sets, Density and Local Bounds
lemmalem:hilbert-triple-penalty-2026aAnalysisPDEFor the penalty function h(x) = (1/2)|x|_V^2 on the small space of a Hilbert triple: h dominates (1/2)|x|_H^2, expands exactly to second order with gradient x in V and Ax in H, has sublevel sets closed in H (so h is lower semicontinuous on V for the metric of H), D(A) meets every…A Linear Perturbation Producing a Sequentially Strict Maximum under a Coercive Bound
corollarycor:perturbed-maximum-linear-hilbert-2026aAnalysisPDEIf a function with closed superlevel sets on a subset of a real Hilbert space is dominated by a constant minus a positive multiple of the squared norm, then subtracting a linear functional of arbitrarily small norm makes it attain a sequentially strict maximum.A Perturbed Maximum Principle of Borwein-Preiss Type in a Real Hilbert Space
theoremthm:perturbed-maximum-hilbert-2026aAnalysisPDEA function bounded above with closed superlevel sets on a subset of a real Hilbert space becomes, after subtracting a single small quadratic, a function attaining a sequentially strict maximum at a point close to any given near-maximiser.The Subspaces Spanned by an Orthonormal Sequence and Exhausting Sequences
lemmalem:orthonormal-basis-exhausting-2026bAnalysisThe spans of the initial segments of an orthonormal sequence are finite-dimensional closed subspaces with an explicit orthogonal projection, and they form an exhausting sequence exactly when the orthonormal sequence is a basis.Orthonormal Expansions in a Real Hilbert Space
theoremthm:orthonormal-expansion-hilbert-2026bAnalysisBessel's inequality, the Riesz-Fischer criterion for convergence of an orthonormal series, and the equivalence of totality, the expansion of every vector, Parseval's identity and density of the finite linear combinations.- An orthonormal sequence in a real Hilbert space is an orthonormal basis if the only vector orthogonal to every member of the sequence is zero; completeness of the space is part of the definition.
The Doubling Form on the Product of a Real Hilbert Space with Itself
lemmalem:doubling-form-product-hilbert-2026aAnalysisPDEThe bilinear form sending a pair of points of the product to the inner product of their differences is a bounded symmetric bilinear form of norm at most two, and the corresponding multiple of the squared distance between coordinates is of class with explicit gradient and He…Properties of the Product of Two Real Inner Product Spaces
lemmalem:product-inner-product-space-2026bAnalysisThe 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-2026bAnalysisLinearity, 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.