Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Derivatives of the Slice of a Function Along a Line
lemmalem:line-slice-derivative-2026bAnalysisMultivariable CalculusLet be a natural number, let be the real numbers, and let be an open subset of Euclidean space . Write for the dot product of points of and for the matrix-vector product. Let be…Derivative of a Finite Linear Combination of Real Functions
lemmalem:derivative-finite-linear-combination-2026aAnalysisLet be the real numbers, let be order-convex, and let satisfy for some , so that is an interior point of and derivatives at in the sense of Derivative at an Interior Point are defined. Let be…Rolle's Theorem and the Mean Value Theorem on a Closed Interval
theoremthm:rolle-mean-value-theorem-2026aAnalysisLet be the real numbers and let be the real line, that is, equipped with the absolute value metric. Let satisfy , let be the closed interval with endpoints and , which is order-convex b…Extreme Value Theorem on a Closed Interval
theoremthm:extreme-value-theorem-closed-interval-2026aAnalysisTopologyLet be the real numbers and let be the real line, that is, equipped with the absolute value metric. Let satisfy , and let be the closed interval with endpoints and . Let…Continuity of a Real Function Agrees with Metric Continuity on the Real Line
lemmalem:continuity-real-metric-agree-2026aAnalysisTopologyLet be the real numbers and let be the real line, that is, equipped with the absolute value metric. Let , let , and let . Then the following two statements are equivalent.…- Let be the real numbers, let be order-convex, let , and let satisfy for some , so that is an interior point of . Suppose that and are real numbers each of which has the propert…
A Semiconvex Function of Class has Hessian Bounded Below by
corollarycor:semiconvex-c2-hessian-bound-2026aAnalysisPDEMultivariable CalculusLet be a natural number and let be the real numbers. Let be an open and convex subset of Euclidean space , a real vector space by Euclidean Space is a Real Vector Space, let satisfy…A Convex Function of Class has Positive Semidefinite Hessian
theoremthm:convex-c2-hessian-psd-2026aAnalysisLinear AlgebraMultivariable CalculusLet be a natural number and let be the real numbers. Let be an open and convex subset of Euclidean space , a real vector space by Euclidean Space is a Real Vector Space, and let be…A Local Minimum of a Convex Function is Global
lemmalem:convex-local-min-global-2026aAnalysisMultivariable CalculusLet be a natural number and let be the ordered field of real numbers. Equip Euclidean space , a real vector space by Euclidean Space is a Real Vector Space, with the Euclidean distance , a metric by…Affine Functions, Sums, Nonnegative Multiples and Pointwise Suprema of Convex Functions
lemmalem:convex-function-operations-2026aAnalysisMultivariable CalculusLet be a natural number, let be the ordered field of real numbers, and let be convex, where Euclidean space is a real vector space by Euclidean Space is a Real Vector Space. Then the following hold, conv…Euclidean Balls are Convex
lemmalem:euclidean-ball-convex-2026aAnalysisTopologyMultivariable CalculusLet be a natural number and let be the ordered field of real numbers. Equip Euclidean space with the Euclidean distance , a metric by Euclidean Distance is a Metric on . Let and let satisfy…Linearity of the Matrix-Vector Product and the Quadratic Form as a Double Sum
lemmalem:matrix-vector-linearity-2026aAnalysisLinear AlgebraMultivariable CalculusLet be a natural number and let be the real numbers. Let be real matrices, with entries and so on, let be points of Euclidean space , and let . Write for the sum of matrices, f…Bilinearity and Symmetry of the Dot Product on
lemmalem:dot-product-bilinear-2026aAnalysisLinear AlgebraMultivariable CalculusLet be a natural number and let be the real numbers. Regard Euclidean space as a real vector space by Euclidean Space is a Real Vector Space, with the sum of points and the scalar multiple , and write and…Concatenation Identifies a Product of Euclidean Spaces with a Euclidean Space
lemmalem:euclidean-concatenation-2026aAnalysisLinear AlgebraMultivariable CalculusLet be natural numbers and let be the ordered field of real numbers. For regard Euclidean space as a real vector space by Euclidean Space is a Real Vector Space, with the sum , the…- Let be a field, let be the set of natural numbers, ordered by the relations of Order on the Natural Numbers, and for let be the initial segment determined by , that is, the set of with . Sums below are the…
Semiconvex Function on a Convex Subset of
definitiondef:semiconvex-function-rn-2026aAnalysisPDEMultivariable CalculusLet be a natural number, let be the real numbers, let be convex, let , and let satisfy . Write for the Euclidean norm on . We say that is…Convex Real-Valued Function on a Convex Subset of
definitiondef:convex-function-rn-2026aAnalysisMultivariable CalculusLet be a natural number, let be the real numbers, let be convex, and let . We say that is convex on if for all and every with and ,…- Let be a natural number, let be the ordered field of real numbers, and regard Euclidean space as a real vector space by Euclidean Space is a Real Vector Space, with the sum of points and the scalar multiple . A…
Comparison Principle for First-Order Strictly Proper Equations by Doubling of Variables
theoremthm:comparison-first-order-strictly-proper-2026bAnalysisPDEDoubling of variables yields comparison on a bounded domain for a strictly proper operator that does not depend on the matrix argument and satisfies a structure condition with a modulus of continuity.Comparison of a Viscosity Subsolution with a Strict Classical Supersolution
theoremthm:comparison-c2-strict-supersolution-2026bAnalysisPDEOn a bounded domain, a viscosity subsolution of a proper operator lies below any lower semicontinuous strict classical supersolution that dominates it on the boundary.