Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Cauchy-Schwarz Inequality in a Real Inner Product Space
theoremthm:cauchy-schwarz-real-2026aAnalysisLinear AlgebraIn a real inner product space, |<x,y>| is at most |x||y|.Elementary Identities in a Real Inner Product Space
lemmalem:real-inner-product-identities-2026aAnalysisLinear AlgebraBilinearity in the second argument, behaviour of the zero vector, vanishing and homogeneity of the norm, the expansions of |x±y|^2, the parallelogram law and the polarisation identity.- Defines real inner product spaces, the norm |x| as the nonnegative square root of <x,x>, and the distance d(x,y)=|x-y|.
Perron's Method: Existence of a Viscosity Solution of the Dirichlet Problem
theoremthm:perron-existence-2026aAnalysisPDEIf comparison holds for the Dirichlet problem and there are a bounded subsolution and a bounded supersolution whose envelopes attain the boundary data, then the supremum of all subsolutions between them is a viscosity solution of the Dirichlet problem.The Bump Construction: Raising a Subsolution Whose Lower Envelope Fails the Supersolution Inequality
lemmalem:perron-bump-2026aAnalysisPDEIf the lower semicontinuous envelope of a viscosity subsolution fails the supersolution inequality at an interior point, then the subsolution can be raised strictly somewhere near that point, by a modification supported in an arbitrarily small ball, without losing the subsolution…The Maximum of Two Viscosity Subsolutions is a Viscosity Subsolution
corollarycor:max-two-subsolutions-2026aAnalysisPDEThe pointwise maximum of two viscosity subsolutions of a continuous second-order equation operator is again a viscosity subsolution.The Upper Semicontinuous Envelope of a Supremum of Viscosity Subsolutions is a Viscosity Subsolution
lemmalem:sup-of-subsolutions-2026aAnalysisPDEIf a nonempty family of viscosity subsolutions of a continuous second-order equation operator is locally uniformly bounded above, then the upper semicontinuous envelope of its pointwise supremum is again a viscosity subsolution.A Viscosity Solution of the Dirichlet Problem is Continuous and Attains the Boundary Data
propositionprop:dirichlet-solution-basic-2026aAnalysisPDEA viscosity solution of the Dirichlet problem equals the boundary data on the boundary, is continuous on the closure, and restricts to a viscosity solution of the equation on the open set.Viscosity Sub- and Supersolutions and Solutions of the Dirichlet Problem
definitiondef:dirichlet-problem-viscosity-2026aAnalysisPDEA viscosity subsolution of the Dirichlet problem is a viscosity subsolution up to the boundary that lies below the boundary data there; dually for supersolutions, and a solution is both.The Viscosity Sub- and Supersolution Properties are Local
lemmalem:viscosity-subsolution-local-2026aAnalysisPDEA viscosity subsolution restricts to a viscosity subsolution on any open subset, and conversely a function that is a viscosity subsolution on an open neighbourhood of each point of the domain is a viscosity subsolution on the whole domain. The same holds for supersolutions.Sequential Form of the Continuity of a Second-Order Equation Operator
lemmalem:operator-sequential-continuity-2026aAnalysisPDEIf a second-order equation operator is continuous at a quadruple and each of the four arguments is approached by a convergent sequence, then the values of the operator converge to its value at that quadruple.Restriction of a Second-Order Equation Operator to an Open Subset
lemmalem:operator-restriction-2026aAnalysisPDERestricting the spatial variable of a second-order equation operator to an open subset again gives a second-order equation operator, and degenerate ellipticity and continuity are inherited.Continuity of the Value, Gradient and Hessian Maps of a Differentiable Function
lemmalem:test-data-continuous-2026aAnalysisMultivariable CalculusFor a function of class the gradient map is continuous, and for a function of class both the gradient map into and the Hessian map into the symmetric matrices with their norm distance are continuous.Semicontinuity and the Semicontinuous Envelopes are Local Notions
lemmalem:semicontinuity-envelope-localisation-2026aAnalysisTopologyWhether a function is semicontinuous at a point, and the values of its semicontinuous envelopes near that point, depend only on the restriction of the function to a closed ball around it.- The pointwise maximum of two functions upper semicontinuous at a point is upper semicontinuous there, and dually the pointwise minimum of two lower semicontinuous functions is lower semicontinuous.
The Subsequence Criterion for Convergence in a Metric Space
lemmalem:subsequence-criterion-convergence-metric-2026aAnalysisTopologyA subsequence of a subsequence is a subsequence. If every subsequence of a sequence in a metric space has in turn a subsequence converging to a fixed point, then the whole sequence converges to that point.Continuity Between Metric Spaces is Equivalent to Sequential Continuity
lemmalem:sequential-continuity-metric-2026bAnalysisTopologyA map from a subset of a metric space into a metric space is continuous at a point relative to the subset exactly when it carries sequences in the subset converging to the point to sequences converging to its value; likewise on the whole subset.- Finitely many maps continuous at a point admit a single modulus: one works for all of them. A finite sum of terms each at most is at most , where is the sum of ones.
The Quartic Bump: Making a Local Maximum Strict without Changing the Test Data
lemmalem:quartic-bump-strict-maximum-2026aAnalysisMultivariable CalculusThe function is of class with vanishing gradient and Hessian at , and is positive away from . Adding it to a test function turns a local maximum at into a strict one while leaving the gradient and Hessian at unchanged.Properties of the Lower Semicontinuous Envelope, by Duality
lemmalem:lsc-envelope-properties-2026aAnalysisTopologyThe lower semicontinuous envelope is the negative of the upper semicontinuous envelope of the negated function; from this it is dominated by the function, is lower semicontinuous, is the greatest lower semicontinuous minorant, is a fixed point exactly for lower semicontinuous fun…