Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Continuously Differentiable Map Whose Jacobian Matrix is Close to the Identity Maps a Cube into a Slightly Larger Cube
lemmalem:near-identity-cube-2026aMultivariable CalculusIf every entry of the Jacobian matrix of a C^1 map differs from the identity by at most eta/d on a closed cube of half-side r, the map sends the cube into the cube about the image of the centre with half-side (1+eta)r.The Gradient of a Twice Continuously Differentiable Function with Hessian Pinched between Two Positive Multiples of the Identity is a Bi-Lipschitz Bijection of Euclidean Space with Continuously Differentiable Inverse
lemmalem:gradient-diffeomorphism-strongly-convex-2026aMultivariable CalculusFor a C^2 function whose Hessian is pinched between epsilon and L times the identity, the gradient map is a bi-Lipschitz bijection of Euclidean space whose inverse has C^1 components, with Jacobian matrix the inverse of the Hessian.Change of Variables for the Lebesgue Integral under a Continuously Differentiable Bijection of Euclidean Space with Symmetric Positive Definite Jacobian Matrix, and the Density of a Push-Forward
theoremthm:change-of-variables-diffeomorphism-euclidean-2026aAnalysisMultivariable CalculusFor a bijection F of Euclidean space whose components and inverse components are continuously differentiable, with symmetric positive definite Jacobian matrix, the integral of f equals the integral of (f composed with F) times det DF for every nonnegative or integrable Borel f, a…Term-by-Term Differentiation of a Series of Continuously Differentiable Functions with Summable Uniform Bounds
lemmalem:series-c1-functions-euclidean-2026aAnalysisMultivariable CalculusA series of C^1 functions on R^q whose values and partial derivatives are dominated by summable constants converges to a C^1 function whose partial derivatives are the series of the partial derivatives, with the summed constants as bounds.The Gaussian Kernels on Euclidean Space: Scaling, Derivatives up to Order Three, the Convolution Identity, Moments and Tails
lemmalem:gaussian-kernel-euclidean-2026aAnalysisMultivariable CalculusFor 0<s<=1 the normalised Gaussian g_s on R^q scales as s^{-q/2}g_1(z/sqrt(s)), is smooth and even, has explicit partial derivatives up to order three with uniform and square-integral bounds of the expected powers of s, satisfies the convolution identity g_s*g_s=g_{2s}, has secon…Test Functions on Euclidean Space, Their Gradient Maps and Laplacians
definitiondef:test-function-euclidean-2026aAnalysisMultivariable CalculusA test function on R^q is a smooth, compactly supported real-valued function; the set of test functions is written C_c^infty(R^q). The gradient map of a test function sends x to the gradient at x, and its Laplacian is the Laplacian of a C^2 function.Existence of a Smooth Plateau Function on Euclidean Space
lemmalem:smooth-plateau-euclidean-2026aAnalysisMultivariable CalculusFor a centre x0 and radii r < s there is a smooth function on R^q with values in [0,1] that equals 1 on the closed ball of radius r about x0 and vanishes wherever the distance to x0 is at least s. This is the bump-function lemma restated for the current (recursive C^k) notion of…Scaled Cutoffs and the Second-Moment Test Functions: Uniform Derivative Bounds and Agreement on a Ball
lemmalem:cutoff-second-moment-test-functions-2026aAnalysisMultivariable CalculusRescaling a smooth bump function by a radius R gives smooth compactly supported cutoffs whose first and second partial derivatives are bounded by constants times 1/R and 1/R^2; multiplying the cutoff by half the squared norm gives smooth compactly supported functions whose gradie…Integration by Parts on Euclidean Space Against a Compactly Supported Function of Class
lemmalem:integration-by-parts-euclidean-2026aAnalysisMultivariable CalculusThe partial derivative of a compactly supported C^1 function on R^q integrates to zero, and consequently the integral of f times a partial derivative of g equals minus the integral of the same partial derivative of f times g whenever f and g are of class C^1 and g is compactly su…The Integral over the Unit Cell of a Product of One-Variable Functions
lemmalem:product-function-integral-cell-2026aAnalysisMultivariable CalculusFor bounded Borel functions of one variable, the integral over the torus of the product of their coordinate evaluations is the product of their integrals over the unit interval.Convolution of a Locally Integrable Function with a Compactly Supported Kernel
lemmalem:kernel-convolution-locally-integrable-2026aAnalysisMultivariable CalculusThe convolution of a function integrable on every bounded set with a continuous kernel vanishing outside a ball is defined at every point, is continuous, is linear in each argument, and is as differentiable as the kernel, the derivatives falling on the kernel.The Laplacian of a Twice Continuously Differentiable Function
definitiondef:laplacian-euclidean-2026aAnalysisMultivariable CalculusDefines the Laplacian of a twice continuously differentiable function on a Euclidean open set as the sum of its unmixed second partial derivatives.Elementary Properties of Lattice-Periodic Functions
lemmalem:periodic-function-basic-2026aAnalysisMultivariable CalculusPeriodic functions are closed under sums, scalar multiples and products; the partial derivatives of a periodic function are periodic; a continuous periodic function is bounded, attaining the largest absolute value on the closed unit cube; and a continuous function vanishing outsi…The Half-Open Unit Cell Tiles Euclidean Space
lemmalem:unit-cell-tiling-2026aAnalysisMultivariable CalculusThe half-open unit cube and its integer translates partition Euclidean space. Records the resulting wrapping map, identifies the interior, closure and measure of the cube, and shows that a periodic function has the same integral over every translate of the cube.Lattice-Periodic Functions and the Periodic Function Classes
definitiondef:periodic-function-lattice-2026aAnalysisMultivariable CalculusDefines the integer lattice in R^n, what it means for a function on R^n to be periodic under it, and the classes of continuous, k-times continuously differentiable, and smooth periodic functions.Continuity of the Value, Gradient and Hessian Maps of a Differentiable Function
lemmalem:test-data-continuous-2026aAnalysisMultivariable CalculusFor a function of class the gradient map is continuous, and for a function of class both the gradient map into and the Hessian map into the symmetric matrices with their norm distance are continuous.The Quartic Bump: Making a Local Maximum Strict without Changing the Test Data
lemmalem:quartic-bump-strict-maximum-2026aAnalysisMultivariable CalculusThe function is of class with vanishing gradient and Hessian at , and is positive away from . Adding it to a test function turns a local maximum at into a strict one while leaving the gradient and Hessian at unchanged.Concatenation and the Sup-Convolution of a Sum in Separated Variables
lemmalem:sup-convolution-separate-variables-2026aAnalysisMultivariable CalculusRecords that concatenation carries origins to the origin and is compatible with coordinatewise convergence, and shows that the sup-convolution of a function of the form is the sum of the sup-convolutions of and with the same parameter.Differential Calculus and Convexity on Euclidean Open Sets: Standing Notation
settingset:euclidean-calculus-2026aAnalysisMultivariable CalculusFixes the standing notation for partial derivatives, functions of class , gradients and Hessians, twice differentiability at a point in the second-order expansion sense, continuity, semicontinuity and local extrema, and convex and semiconvex functions on Euclidean space.Localisation of an Upper Semicontinuous Function by Projection onto a Closed Ball
lemmalem:usc-ball-localisation-2026aAnalysisMultivariable CalculusDescribes the nearest point projection onto a closed ball centred at the origin and shows that composing an upper semicontinuous function with it, minus a multiple of the excess of the squared norm over the squared radius, produces an upper semicontinuous function on all of Eucli…