Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…The Proximal Map of a Convex Function on
definitiondef:proximal-map-convex-rn-2026aAnalysisMultivariable CalculusDefines the proximal map of a convex function on Euclidean space, sending a point to the unique minimiser of .Existence and Uniqueness of the Proximal Minimiser of a Convex Function
lemmalem:proximal-minimiser-rn-2026aAnalysisMultivariable CalculusFor a convex function on Euclidean space and any point , the function attains its minimum at exactly one point.Elementary Calculus of the Subdifferential of a Convex Function
lemmalem:subdifferential-calculus-convex-rn-2026aAnalysisMultivariable CalculusSubgradients of a convex function on an open convex set are monotone, are bounded by a local Lipschitz constant, have closed graph, reduce to the gradient at a point of differentiability, and depend continuously on the base point wherever the subgradient is unique.The Subdifferential of a Convex Function on an Open Convex Set is Nonempty
theoremthm:subdifferential-nonempty-interior-rn-2026aAnalysisMultivariable CalculusA convex function on an open convex subset of Euclidean space has a subgradient at every point, obtained from a supporting hyperplane to a bounded piece of its epigraph; and a subgradient inequality valid on one closed ball around the point is automatically valid on the whole set…- A Lipschitz function on Euclidean space is differentiable outside a Borel null set, with derivative the vector of its partial derivatives and with gradient bounded by the Lipschitz constant; the same holds for locally Lipschitz maps into on an open set.
A Borel Set Whose Lines in One Coordinate Direction Are Null Is Null
lemmalem:null-sections-coordinate-rn-2026aAnalysisMultivariable CalculusIf every line in a fixed coordinate direction meets a Borel subset of Euclidean space in a one-dimensional null set, then the set itself has Lebesgue measure zero.The Partial Derivatives of a Lipschitz Function on Exist Almost Everywhere
lemmalem:lipschitz-partial-derivatives-ae-rn-2026aAnalysisMultivariable CalculusFor a Lipschitz function on Euclidean space and a fixed coordinate direction, the Borel set where the corresponding partial derivative fails to exist is null, and where it exists it is bounded by the Lipschitz constant.Borel Structure of the Set Where a Partial Derivative Exists
lemmalem:partial-derivative-sets-borel-rn-2026aAnalysisMultivariable CalculusFor a continuous function on Euclidean space, the closed sets on which all small rational difference quotients in a coordinate direction agree to within exhaust the set where that partial derivative exists, which is therefore Borel, and on them the difference quotients appr…Near a Density Point Every Direction Meets the Set Closely
lemmalem:density-point-nearby-rn-2026aAnalysisMultivariable CalculusIf is a density point of a set then, for points close enough to , the set comes within a prescribed fraction of the distance from to of the point .- Almost every point of an arbitrary subset of Euclidean space is a density point of that subset; no measurability of the set is assumed, the statement being formulated with Lebesgue outer measure.