Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Differential Calculus and Convexity on Euclidean Open Sets: Standing Notation
settingset:euclidean-calculus-2026aAnalysisMultivariable CalculusFixes the standing notation for partial derivatives, functions of class , gradients and Hessians, twice differentiability at a point in the second-order expansion sense, continuity, semicontinuity and local extrema, and convex and semiconvex functions on Euclidean space.Euclidean Space and Real Matrices: Standing Notation (Algebra)
settingset:real-matrices-2026cLinear AlgebraStanding notation for Euclidean space and real matrices, extending the routine toolkit: R^n with its dot product, norm and distance, matrices and their algebra, standard basis vectors, block matrices, trace, determinant, adjugate, inverses, diagonal and orthogonal matrices, each…Localisation of an Upper Semicontinuous Function by Projection onto a Closed Ball
lemmalem:usc-ball-localisation-2026aAnalysisMultivariable CalculusDescribes the nearest point projection onto a closed ball centred at the origin and shows that composing an upper semicontinuous function with it, minus a multiple of the excess of the squared norm over the squared radius, produces an upper semicontinuous function on all of Eucli…Quadratic Test Functions, Limits, Translation and Locality for Approximability by Test Data
lemmalem:test-data-basic-2026aAnalysisPDEApproximability by test data can always be realised with quadratic test functions; it follows at a point of twice differentiability, is stable under limits of the approximating data, transforms predictably under translation and affine perturbation, and depends only on the values…Twice Differentiability of a Sum in Separated Variables
lemmalem:twice-differentiable-separated-2026aAnalysisMultivariable CalculusA sum in separated variables is twice differentiable at a point exactly when both summands are, and its Hessian is then the block diagonal matrix built from their Hessians; in particular the off-diagonal block vanishes.Quadratic and Affine Functions of Class , Translation, and Quadratic Perturbation of Semiconvexity
lemmalem:quadratic-affine-c2-2026aAnalysisMultivariable CalculusThe function obtained from a symmetric matrix, a vector and a constant is of class with the expected gradient and Hessian; class and its derivatives are preserved by translation; positive semidefinite quadratic forms are convex; and subtracting a quadratic form from a…Block Diagonal Symmetric Matrices and the Blocks of a Symmetric Matrix
lemmalem:block-diagonal-symmetric-2026aLinear AlgebraFor a splitting of a dimension into two parts, records the symmetry, quadratic form, norm, distance and ordering of block diagonal symmetric matrices, and identifies the three blocks of an arbitrary symmetric matrix.Limits and Bounded Sequences of Symmetric Real Matrices
lemmalem:symmetric-matrix-limits-2026aAnalysisLinear AlgebraA norm-bounded sequence of symmetric real matrices has a convergent subsequence; quadratic forms depend continuously on the matrix; the positive semidefinite ordering passes to limits; and two-sided order bounds give a norm bound.Sums, Differences and Scalar Multiples of Functions Twice Differentiable at a Point
lemmalem:twice-differentiable-sum-2026aAnalysisMultivariable CalculusTwice differentiability at a point, in the second-order expansion sense, is preserved by sums, differences and scalar multiples, with the first-order coefficients and Hessians combining in the same way.A Weighted Young Inequality and the Splitting of a Quadratic Form
lemmalem:quadratic-form-splitting-2026aAnalysisLinear AlgebraRecords the weighted Young inequality for the dot product and deduces the inequality comparing the quadratic form of a symmetric matrix at a point with its value at a second point, with a squared-distance penalty.Vector, Entry and Comparison Bounds for the Norm of a Symmetric Real Matrix
lemmalem:symmetric-matrix-norm-bounds-2026aLinear AlgebraRelates the norm of a symmetric real matrix to its action on vectors and to its entries, and records the identity for the norm of an image together with a comparison bound for quadratic forms.Alexandrov's Theorem for Semiconvex Functions on an Open Convex Set
corollarycor:alexandrov-open-semiconvex-rn-2026aAnalysisMultivariable CalculusA semiconvex function with constant on an open convex subset of Euclidean space is twice differentiable outside a null set, and wherever it is twice differentiable its Hessian is bounded below by .Alexandrov's Theorem: a Convex Function on is Twice Differentiable Almost Everywhere
theoremthm:alexandrov-convex-rn-2026aAnalysisMultivariable CalculusA convex function on Euclidean space admits a second-order expansion with a symmetric Hessian at every point outside a Borel null set, and wherever it is twice differentiable its Hessian is positive semidefinite.A First-Order Expansion of the Subdifferential Gives a Second-Order Expansion of the Function
lemmalem:subgradient-expansion-twice-differentiable-rn-2026aAnalysisMultivariable CalculusIf the subgradients of a convex function admit a first-order expansion about a point with matrix , then the function admits a second-order expansion there with Hessian the symmetric part of ; this is obtained by telescoping the subgradient inequalities along a segment.Basic Properties of Twice Differentiability at a Point
lemmalem:twice-differentiable-basic-rn-2026aAnalysisMultivariable CalculusAt a point of twice differentiability the first-order coefficient is the gradient; a function of class is twice differentiable at every point, with the usual gradient and Hessian; and at a local maximum the gradient vanishes and the Hessian is negative semidefinite.Twice Differentiability at a Point
definitiondef:twice-differentiable-at-point-rn-2026aAnalysisMultivariable CalculusDefines twice differentiability of a real-valued function at a point of an open subset of Euclidean space, by a second-order expansion with a symmetric Hessian, the coefficients being unique.A Symmetric Matrix is Determined by its Quadratic Form, and a Second-Order Expansion by its Coefficients
lemmalem:second-order-expansion-unique-rn-2026aLinear AlgebraMultivariable CalculusTwo symmetric matrices with the same quadratic form are equal; consequently the linear and quadratic coefficients of a second-order expansion of a function at a point are uniquely determined.An Injective Nondegenerate Square Matrix is Invertible
lemmalem:square-matrix-injective-invertible-rn-2026aAnalysisLinear AlgebraIf the map determined by a real square matrix is injective it satisfies a lower bound and has closed convex image; if in addition no unit vector annihilates that image, the matrix is surjective and hence invertible, with an inverse obeying the reciprocal bound.Extending a Convex Function from a Closed Ball to All of
lemmalem:convex-extension-from-ball-rn-2026aAnalysisMultivariable CalculusThe supremum of the affine minorants furnished by the subgradients at points of a closed ball is a convex Lipschitz function on all of Euclidean space that agrees with the given convex function on that ball.Properties of the Proximal Map of a Convex Function
lemmalem:proximal-map-properties-rn-2026aAnalysisMultivariable CalculusThe proximal map of a convex function has fibres described by the subdifferential, is surjective, is firmly nonexpansive and hence Lipschitz with constant one, and wherever it is differentiable its derivative matrix satisfies and is injectiv…