Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Comparison Principle for the Dirichlet Problem for Second-Order Equations
theoremthm:comparison-dirichlet-second-order-2026aAnalysisPDEFor a continuous, strictly proper operator satisfying the structure condition, a viscosity subsolution up to the boundary that lies below a viscosity supersolution on the boundary of a bounded domain lies below it throughout the closure.Ishii's Lemma: Test Data and Matrix Bounds at a Maximum of a Quadratically Penalised Difference
lemmalem:ishii-doubling-2026aAnalysisPDEAt a local maximum of there are symmetric matrices and giving test data from above for and from below for , both with first-order coefficient , and satisfying the two-sided bound…The Doubling Matrix and its Elementary Properties
lemmalem:doubling-matrix-2026aAnalysisLinear AlgebraCollects the properties of the block matrix with diagonal blocks and off-diagonal blocks : its action on concatenated vectors, its quadratic form , the bounds , the identity , and the fact that…- A quadruple is approximable by test data from above for a function exactly when the sign-reversed quadruple is approximable from below for the negated function, and symmetrically.
Continuity of a Second-Order Equation Operator
definitiondef:continuous-second-order-operator-2026aAnalysisPDEDefines continuity of a second-order equation operator at a quadruple , and continuity on its whole domain, in terms of the Euclidean distance, the absolute value, the Euclidean norm and the distance between symmetric matrices.Reduction of the Theorem on Sums to a Global Quadratic Bound
lemmalem:theorem-on-sums-reduction-2026aAnalysisPDENormalises the data of the theorem on sums by translation and an affine correction and localises the summands to a closed ball, producing upper semicontinuous functions bounded above on the whole space that vanish at the origin, satisfy a global quadratic bound with matrix…The Theorem on Sums for a Global Quadratic Bound, in Two Groups of Variables
theoremthm:theorem-on-sums-global-quadratic-2026aAnalysisPDEFor upper semicontinuous functions bounded above, vanishing at the origin and satisfying globally, produces for each symmetric matrices that are admissible second-order test d…Second-Order Test Data at a Global Quadratic Maximum of a Semiconvex Function
lemmalem:semiconvex-quadratic-maximum-hessian-2026aAnalysisPDEFor a semiconvex function on whose difference with a quadratic form attains a maximum at the origin, produces points of twice differentiability approaching the origin whose gradients tend to zero and whose Hessians converge to a symmetric matrix with…Transfer of Approximating Test Data from the Sup-Convolution to the Original Function
lemmalem:sup-convolution-test-data-transfer-2026aAnalysisPDEShows that test data approximable from above for the sup-convolution at a point with first-order datum transfers to the same first-order and second-order data for itself at , together with the accompanying identity for the…Concatenation and the Sup-Convolution of a Sum in Separated Variables
lemmalem:sup-convolution-separate-variables-2026aAnalysisMultivariable CalculusRecords that concatenation carries origins to the origin and is compatible with coordinatewise convergence, and shows that the sup-convolution of a function of the form is the sum of the sup-convolutions of and with the same parameter.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.Real Matrices, Symmetric Matrices and the Semidefinite Ordering: Standing Notation
settingset:real-matrices-2026aLinear AlgebraFixes the standing notation for real matrices and their algebra, for symmetric matrices, for the positive semidefinite ordering, for the norm and distance on symmetric matrices, for the standard basis vectors, and for concatenation and block matrices.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.