Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Membership in the Line ℝx₀ of a Real Vector Space
helperhlp:line-membership-real-vector-space-2026aAnalysisA class lies in the line ℝx₀ exactly when it equals tx₀ for some real t.Membership and the Zero Law of a Real Vector Space in Flat Form
helperhlp:vector-space-flat-rules-2026aAnalysisSums and scalar multiples of vectors lie in the space, and the zero vector is neutral on the left.At a Point of Differentiability, the Subdifferential of a Convex Function on an Open Convex Subset of Is the Gradient Alone
lemmalem:subgradient-differentiable-rn-2026aAnalysisIf a convex function on an open convex set is differentiable at a point, its gradient there is a subgradient, and it is the only one.Properties of the Subdifferential on : Minimisers, Convexity and Closedness, Sums and Positive Multiples
lemmalem:subgradient-properties-rn-2026aAnalysisA point minimises f exactly when 0 is a subgradient there; the subdifferential is convex and closed; subgradients of two functions add up to a subgradient of the sum; and subdifferentials scale with positive multiples.A Convex Function on a Convex Subset of Has a Subgradient at Every Interior Point
theoremthm:subgradient-exists-interior-rn-2026aAnalysisAt an interior point of its convex domain, a convex function has a nonempty subdifferential; the subgradient comes from a supporting hyperplane of the epigraph.Subgradients and the Subdifferential of a Real-Valued Function on a Subset of
definitiondef:subgradient-rn-2026aAnalysisA subgradient of f at x is a vector a for which the affine function f(x) + a.(y - x) lies below f on its whole domain; the subdifferential is the set of all subgradients.A Local Minimum of a Convex Function on a Convex Subset of Is a Global Minimum
lemmalem:convex-local-minimum-global-rn-2026aAnalysisIf a convex function on a convex set takes at a point a value no larger than its values at nearby points of the set, that value is no larger than all its values on the set.- A convex function evaluated at a convex combination of finitely many points is at most the same convex combination of its values.
Operations Preserving Convexity of Functions on : Affine Functions, Sums, Nonnegative Multiples, Pointwise Suprema and Affine Substitution
lemmalem:convex-function-operations-rn-2026aAnalysisAffine functions are convex, and sums, nonnegative multiples, pointwise suprema and compositions with affine maps of convex functions are convex.A Function on a Convex Subset of Is Convex If and Only If Its Epigraph Is Convex
lemmalem:convex-epigraph-rn-2026aAnalysisA real-valued function on a convex subset of R^n is convex exactly when its epigraph is a convex subset of R^{n+1}.- The epigraph of a function f on a subset C of R^n is the set of points (x, mu) of R^{n+1} with x in C and mu at least f(x).
- A real-valued function on a convex subset of R^n is convex if its value at every point of a segment is at most the corresponding combination of its values at the endpoints.
- Standing notation for convex functions on subsets of R^n: the separation notation, and points of R^{n+1} written as pairs (x, mu) by concatenation.
Strong Separation of a Closed Convex Set and a Disjoint Compact Convex Set in
theoremthm:strong-separation-rn-2026bAnalysisA nonempty closed convex subset and a disjoint nonempty compact convex subset of R^n are strongly separated by a hyperplane.- Two nonempty disjoint convex subsets of R^n are separated by a hyperplane: some nonzero a and real α satisfy a·x ≤ α ≤ a·y for x in the first set and y in the second.
- If x is not an interior point of a convex subset C of R^n, some unit vector a satisfies a·z ≤ a·x on C; if moreover x lies in the closure of C, a hyperplane through x supports C there.
A Closed Convex Subset of Is the Intersection of the Closed Half-Spaces Containing It
corollarycor:closed-convex-half-spaces-rn-2026bAnalysisA point lies in a closed convex subset C of R^n exactly when it lies in every closed half-space a·y ≤ α that contains C.Strong Separation of a Point from a Closed Convex Subset of
theoremthm:point-separation-closed-convex-rn-2026bAnalysisA point outside a closed convex subset C of R^n is strongly separated from C by a hyperplane, with normal x − p for the nearest point p when C is nonempty.A Point Outside the Interior of a Closed Convex Subset of Has a Supporting Unit Normal
lemmalem:support-closed-convex-rn-2026aAnalysisIf C is a closed convex subset of R^n and x is not an interior point of C, some unit vector a satisfies a·z ≤ a·x for every z in C.Nearest Points in a Nonempty Closed Convex Subset of : Existence, Uniqueness and the Variational Inequality
lemmalem:nearest-point-closed-convex-rn-2026aAnalysisEvery point of R^n has exactly one nearest point in a nonempty closed convex set C, and a point p of C is nearest to x exactly when (x−p)·(y−p) ≤ 0 for all y in C.