Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Proximal Map of a Convex Function on
definitiondef:proximal-map-convex-rn-2026aAnalysisMultivariable CalculusDefines the proximal map of a convex function on Euclidean space, sending a point to the unique minimiser of .Existence and Uniqueness of the Proximal Minimiser of a Convex Function
lemmalem:proximal-minimiser-rn-2026aAnalysisMultivariable CalculusFor a convex function on Euclidean space and any point , the function attains its minimum at exactly one point.Elementary Calculus of the Subdifferential of a Convex Function
lemmalem:subdifferential-calculus-convex-rn-2026aAnalysisMultivariable CalculusSubgradients of a convex function on an open convex set are monotone, are bounded by a local Lipschitz constant, have closed graph, reduce to the gradient at a point of differentiability, and depend continuously on the base point wherever the subgradient is unique.The Subdifferential of a Convex Function on an Open Convex Set is Nonempty
theoremthm:subdifferential-nonempty-interior-rn-2026aAnalysisMultivariable CalculusA convex function on an open convex subset of Euclidean space has a subgradient at every point, obtained from a supporting hyperplane to a bounded piece of its epigraph; and a subgradient inequality valid on one closed ball around the point is automatically valid on the whole set…- A Lipschitz function on Euclidean space is differentiable outside a Borel null set, with derivative the vector of its partial derivatives and with gradient bounded by the Lipschitz constant; the same holds for locally Lipschitz maps into on an open set.
A Borel Set Whose Lines in One Coordinate Direction Are Null Is Null
lemmalem:null-sections-coordinate-rn-2026aAnalysisMultivariable CalculusIf every line in a fixed coordinate direction meets a Borel subset of Euclidean space in a one-dimensional null set, then the set itself has Lebesgue measure zero.The Partial Derivatives of a Lipschitz Function on Exist Almost Everywhere
lemmalem:lipschitz-partial-derivatives-ae-rn-2026aAnalysisMultivariable CalculusFor a Lipschitz function on Euclidean space and a fixed coordinate direction, the Borel set where the corresponding partial derivative fails to exist is null, and where it exists it is bounded by the Lipschitz constant.Borel Structure of the Set Where a Partial Derivative Exists
lemmalem:partial-derivative-sets-borel-rn-2026aAnalysisMultivariable CalculusFor a continuous function on Euclidean space, the closed sets on which all small rational difference quotients in a coordinate direction agree to within exhaust the set where that partial derivative exists, which is therefore Borel, and on them the difference quotients appr…Near a Density Point Every Direction Meets the Set Closely
lemmalem:density-point-nearby-rn-2026aAnalysisMultivariable CalculusIf is a density point of a set then, for points close enough to , the set comes within a prescribed fraction of the distance from to of the point .- Almost every point of an arbitrary subset of Euclidean space is a density point of that subset; no measurability of the set is assumed, the statement being formulated with Lebesgue outer measure.
Density Point of an Arbitrary Subset of
definitiondef:density-point-rn-2026aAnalysisMultivariable CalculusDefines a density point of an arbitrary subset of Euclidean space, using Lebesgue outer measure so that no measurability of the set is required.The Lebesgue Measure of a Closed Ball in
lemmalem:closed-ball-measure-rn-2026aAnalysisMultivariable CalculusEvery closed Euclidean ball is a Borel set of finite measure, and its Lebesgue measure equals for a constant that is positive and finite and does not depend on the centre.McShane Extension of a Real-Valued Lipschitz Function on a Metric Space
lemmalem:lipschitz-extension-mcshane-2026aAnalysisA real-valued Lipschitz function on a nonempty subset of a metric space extends to the whole space with the same Lipschitz constant, by the explicit infimum formula of McShane.Growth Bound for a Lipschitz Function with Small Derivative
lemmalem:lipschitz-growth-bound-1d-2026aAnalysisIf a Lipschitz function on an interval has derivative bounded by at every point of a set , its image of has outer measure at most times that of ; consequently a derivative bound holding almost everywhere makes the function Lipschitz with that constant.A Lipschitz Function on an Open Interval is Differentiable Almost Everywhere
corollarycor:lipschitz-differentiable-ae-1d-2026aAnalysisA Lipschitz real function on an open interval has a derivative at every point outside a Lebesgue null set, and that derivative is bounded in absolute value by the Lipschitz constant.A Nondecreasing Function on an Open Interval is Differentiable Almost Everywhere
theoremthm:monotone-differentiable-ae-2026aAnalysisLebesgue's differentiation theorem for monotone functions: a nondecreasing real function on an open interval has a finite derivative at every point outside a Lebesgue null set.- If a family of closed balls finely covers a set of finite Lebesgue outer measure, then finitely many pairwise disjoint balls of the family cover all of the set except a part of arbitrarily small outer measure.
Product Measures and Lebesgue Measure on ℝⁿ: Standing Notation and Background
settingset:euclidean-lebesgue-2026bAnalysisAdopts the integration and product-measure notation settings and lists, clause by clause, the background results on product measures, image measures, Lebesgue measure on ℝⁿ and linear changes of variables; dependent choice is not a standing hypothesis.The Degenerate-Derivative Values of a Locally Lipschitz Map of Form a Null Set
theoremthm:lipschitz-critical-values-null-rn-2026aAnalysisMultivariable CalculusA Lipschitz analogue of Sard's theorem: if is locally Lipschitz on an open subset of , the image of the set of points where is differentiable with derivative of degenerate range is Lebesgue null.Lipschitz Images and Lebesgue Outer Measure in
lemmalem:lipschitz-image-outer-measure-rn-2026aAnalysisA Lipschitz map with constant increases Lebesgue outer measure by a factor of at most ; in particular Lipschitz and locally Lipschitz maps carry null sets to null sets.