Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- 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.- Standing hypotheses for a nonempty bounded open subset of Euclidean space: its closure is compact, and its boundary is the complement of the domain in the closure.
- Standing notation and background facts for second-order equations on open subsets of Euclidean space: the reals, Euclidean space with its metric and topology, symmetric matrices with the positive semidefinite ordering, functions of class with their gradients and Hessians, a…
A Continuous Function on a Closed Interval is Riemann Integrable
corollarycor:continuous-implies-riemann-integrable-2026aAnalysisA function continuous on a closed real interval is Riemann integrable there, and so is its restriction to every nondegenerate closed subinterval. This records, as a citable statement, the integrability already established inside the first part of the fundamental theorem of calcul…Uniqueness of the Limit of a Real Function at a Point of an Interval
lemmalem:limit-function-unique-2026aAnalysisPunctured neighbourhoods of a point of an interval containing at least two points are nonempty, and consequently at most one real number satisfies the defining condition of the limit, so the limit notation is well defined.Constant Sequences and Index-Shifted Sequences of Real Numbers
lemmalem:constant-and-shifted-sequences-2026aAnalysisA constant real sequence converges to its value, and shifting the index of a convergent real sequence by one leaves the limit unchanged.Continuity of the Identity Map, of Powers, and of Polynomial Functions on a Subset of the Real Line
lemmalem:continuity-identity-polynomial-real-2026aAnalysisThe identity map, the natural-number power maps, and the restriction of any polynomial function are continuous on every subset of the real line.Basic Facts about Intervals of the Real Line and Their Interior Points
lemmalem:real-interval-basic-facts-2026aAnalysisCollects the routine facts about intervals used throughout single-variable calculus: that the real line is an interval all of whose points are interior, that closed intervals between points of an interval lie inside it, and that open and closed intervals are intervals with the ex…A Continuous Injective Function on a Closed Interval is Strictly Monotone
problemprob:continuous-injective-strictly-monotone-2026aAnalysisAnalysis level. Injectivity plus continuity on a closed real interval forces strict monotonicity; the whole argument is repeated use of the intermediate value theorem.