Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.
- Standing notation for real analysis and measure theory on Euclidean space: numbers and sequences, the vector, metric and topological structure of , its Borel -algebra, Lebesgue measure and null sets, and conventions for images and Lipschitz maps.
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.- Every Borel subset of is approximated from outside by open sets and from inside by closed sets, and by compact sets when its measure is finite; the outer measure of an arbitrary set is the infimum of the measures of its open supersets.
- The set of points within distance of a centre and within distance of a hyperplane through it has Lebesgue measure at most .
- Introduces the half-open dyadic cells of , records that each generation partitions into countably many cells of measure and small diameter, that two cells are nested or disjoint, and that every open set is a countable disjoint union of dyadi…
Elementary Properties of Lebesgue Outer Measure on
lemmalem:lebesgue-outer-measure-properties-rn-2026aAnalysisLebesgue outer measure agrees with Lebesgue measure on Borel sets, is monotone and countably subadditive, admits Borel measurable hulls, and vanishes exactly on the null sets.Locally Lipschitz Map on a Euclidean Open Set
definitiondef:locally-lipschitz-euclidean-2026aAnalysisMultivariable CalculusDefines a locally Lipschitz map on an open subset of : every point has a closed ball neighbourhood inside the domain on which the map is Lipschitz.- Defines the Lebesgue outer measure of an arbitrary subset of as the infimum of the Lebesgue measures of the Borel sets containing it.
Jensen's Lemma: the Contact Set of a Semiconvex Function at a Strict Maximum has Positive Measure
lemmalem:jensen-maximum-2026aAnalysisPDEMultivariable CalculusFor a semiconvex function with a strict maximum at the centre of a closed ball, the set of points at which some linear perturbation of norm at most attains its maximum is compact of positive Lebesgue measure for all small , so it is contained in no null set, and…A Lipschitz Estimate Between the Maximisers of Two Linear Perturbations of a Semiconvex Function
lemmalem:semiconvex-perturbed-maximiser-lipschitz-2026aAnalysisMultivariable CalculusIf a linear perturbation of a semiconvex function with constant attains its maximum over a closed ball at a point of the concentric half ball, and a second, nearby perturbation attains its maximum somewhere in the ball, then the two perturbing vectors differ by at most…A Maximiser of a Linearly Perturbed Semiconvex Function Yields a Subgradient and a Global Quadratic Lower Bound
lemmalem:semiconvex-maximiser-lower-quadratic-bound-2026aAnalysisMultivariable CalculusIf a semiconvex function with constant has a maximum of its perturbation by a linear form at an interior point of a subset of its domain, then the associated vector is a subgradient of the convexified function there, and the function is bounded below on the whole domain by…Maximisers of Linearly Perturbed Continuous Functions on a Closed Ball: Existence, Localisation, and Compactness of the Contact Set
lemmalem:perturbed-maximiser-contact-set-2026aAnalysisMultivariable CalculusFor a continuous function on a closed Euclidean ball with a strict maximum at the centre, every small linear perturbation attains its maximum, all such maximisers lie near the centre, and the set of them for perturbations of norm at most a given bound is compact.The Lebesgue Measure of a Lipschitz Image of a Compact Subset of
lemmalem:lipschitz-image-compact-lebesgue-bound-2026aAnalysisMultivariable CalculusIf is Lipschitz with constant on a nonempty compact subset of with values in , then the image of is compact and its Lebesgue measure is at most times that of .Uniform Grids on a Half-Open Box and Grid Hulls of a Compact Set in
lemmalem:grid-hull-compact-rn-2026aAnalysisMultivariable CalculusPartitions a half-open box of into congruent half-open cells of prescribed measure and diameter, shows that halving the mesh refines the partition, and shows that the unions of the cells meeting a compact subset decrease to it with Lebesgue measures converging to i…Local Lipschitz Bound and Continuity for a Semiconvex Function on an Open Convex Set
lemmalem:semiconvex-locally-lipschitz-2026aAnalysisMultivariable CalculusA semiconvex function on an open convex subset of Euclidean space is Lipschitz on a closed ball around each of its points, and is therefore continuous, in the explicit epsilon-delta form used by the extreme value theorem.Subdifferential of a Real-Valued Function on a Convex Subset of
definitiondef:subdifferential-convex-rn-2026aAnalysisMultivariable CalculusDefines the subdifferential of a real-valued function on a convex subset of Euclidean space at a point as the set of vectors whose associated affine function minorises the function and agrees with it at that point, and calls its elements subgradients.