Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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.
- 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.