Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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…Properties of the Upper Semicontinuous Envelope
lemmalem:usc-envelope-properties-2026aAnalysisTopologyThe upper semicontinuous envelope dominates the function, is upper semicontinuous, is the least upper semicontinuous majorant, agrees with the function exactly when the function is upper semicontinuous, is monotone in the function, and is approached along a sequence tending to th…Upper and Lower Semicontinuous Envelopes of a Real-Valued Function
definitiondef:semicontinuous-envelopes-2026aAnalysisTopologyFor a real-valued function on a subset of a metric space that is bounded above near each point, the upper semicontinuous envelope is defined pointwise as the infimum of the constants dominating on some closed ball; the lower envelope is defined dually.Comparison of Real Numbers with Arbitrary Positive Slack
lemmalem:epsilon-comparison-real-2026aAnalysisIf for every positive then ; the two dual forms, and the vanishing criterion for a nonnegative number bounded by every positive number.