Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- 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.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.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.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.First-Order Expansion of the Mean-Field Cost about a Stationary Mean-Field Triple and Its Quadratic Lower Bound
lemmalem:mean-field-cost-first-order-identity-2026aAnalysisMultivariable CalculusLet , , , with rate bound , with derivative bound , , , with second-derivative bound (the open set of the cost extension, written in that definition, is written here),…Quadratic Growth of the Mean-Field Hamiltonian in the Control along a Stationary Mean-Field Triple
lemmalem:hamiltonian-quadratic-growth-2026aAnalysisMultivariable CalculusLet , , , with rate bound , with derivative bound , , , with second-derivative bound , , and be as in the definition of a stationary mean-field triple (the open set of t…Hessian Lower Bound for a Test Function Touching a Semiconvex Function from Above
lemmalem:semiconvex-upper-test-hessian-bound-2026aAnalysisPDEMultivariable CalculusLet be a natural number and let be the real numbers with the order of their ordered field structure. Regard Euclidean space as a real vector space, with the sum of points, the scalar multiple, and the…Restriction of a Map to an Open Subset
lemmalem:ck-restriction-open-subset-2026aMultivariable CalculusLet be natural numbers and let be the real numbers. Let be an open subset of Euclidean space and let be open in . Let and , and let…The Squared Euclidean Norm is Smooth
lemmalem:squared-norm-smooth-euclidean-2026aMultivariable CalculusLet be a natural number, let be the real numbers, and let be the Euclidean norm on Euclidean space , which is an open subset of itself by claim 1 of Euclidean Space is Open in Itself, and Maps are Continuous. For…Euclidean Space is Open in Itself, and Maps are Continuous
lemmalem:euclidean-space-open-ck-continuous-2026aMultivariable CalculusLet and be natural numbers and let be the real numbers. Regard Euclidean space as a metric space through the Euclidean distance , which is a metric by Euclidean Distance is a Metric on , and regard as a metri…Coordinatewise Criterion for Continuity of a Map Between Euclidean Spaces
lemmalem:continuity-coordinatewise-euclidean-2026aAnalysisMultivariable CalculusLet and be natural numbers, let be the real numbers, let be a subset of Euclidean space , let with coordinate functions , and let . Each is regarded as a map from int…