Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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-2026aAnalysisTopologyA map between metric spaces is continuous at a point relative to a subset if and only if it carries every sequence in that subset converging to the point to a sequence converging to the image of the point.- 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.The Structure Condition Implies Degenerate Ellipticity
propositionprop:structure-condition-implies-elliptic-2026aAnalysisPDEA continuous second-order equation operator that satisfies the structure condition of the comparison principle for the Dirichlet problem is automatically degenerate elliptic, so the ellipticity hypothesis of that comparison principle is redundant. Only the openness of the domain…Uniqueness for the Dirichlet Problem for a Viscous Hamilton-Jacobi Equation
corollarycor:uniqueness-viscous-hamilton-jacobi-2026aAnalysisPDETwo continuous viscosity solutions on the closure of a bounded domain of the equation that agree on the boundary agree everywhere.The Viscous Hamilton-Jacobi Operator is Continuous, Strictly Proper and Satisfies the Structure Condition
propositionprop:viscous-hamilton-jacobi-operator-2026aAnalysisPDEFor positive , nonnegative and continuous , the operator of the viscous Hamilton-Jacobi equation is continuous, strictly proper with constant , and satisfies th…Structure Condition: the Trace Operator of a Lipschitz Diffusion Coefficient
exampleex:structure-condition-trace-diffusion-2026aAnalysisPDEThe linear second-order operator satisfies the structure condition of the comparison principle with the linear modulus , whenever the coefficient is Lipschitz with constant in the row-sum-…Structure Condition: a Linear First-Order Operator with an Almost Monotone Drift
exampleex:structure-condition-monotone-drift-2026aAnalysisPDEThe first-order operator satisfies the structure condition of the comparison principle, with the linear modulus , whenever , that is, whenever becomes monotone after adding times the id…Structure Condition: a Degenerate Elliptic Operator with a Continuous Inhomogeneity
exampleex:structure-condition-continuous-inhomogeneity-2026aAnalysisPDEIf is degenerate elliptic in the matrix variable and is continuous on the closure of the domain, then satisfies the structure condition of the comparison principle, with a modulus of continuity for as modulus.- For a nonnegative real constant , the map on the nonnegative reals is a modulus of continuity, and it is nondecreasing.
A Continuous Function on a Compact Set Admits a Nondecreasing Modulus of Continuity
lemmalem:modulus-of-continuity-compact-2026aAnalysisTopologyA real-valued continuous function on a nonempty compact subset of a metric space admits a modulus of continuity that is nondecreasing and dominates the oscillation of the function at every scale.The Trace as a Sum of Quadratic Forms, its Monotonicity and a Norm Bound
lemmalem:trace-quadratic-forms-2026aLinear AlgebraFor a real matrix with rows and a symmetric , the trace of is the sum of the quadratic forms . Consequences: the trace of a symmetric matrix is the sum of its diagonal quadratic forms, it is monotone for the semidefi…Uniqueness for the Dirichlet Problem for Second-Order Equations
corollarycor:uniqueness-dirichlet-second-order-2026aAnalysisPDETwo continuous viscosity solutions on a bounded domain that agree on the boundary agree throughout the closure, for a continuous, strictly proper operator satisfying the structure condition.