Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- On the torus, which has total measure one, a function power-integrable for a larger exponent is power-integrable for a smaller one, with a smaller seminorm.
Finite Sums of Real Numbers: Nonnegativity, Domination by the Sum, and Limits
lemmalem:finite-sum-real-basic-2026aAnalysisA finite sum of nonnegative real numbers is nonnegative and dominates each of its terms, and a finite sum of convergent real sequences converges to the sum of the limits.The Square-Integrable and Sobolev Spaces of the Torus Form a Hilbert Triple
lemmalem:sobolev-hilbert-triple-torus-2026aAnalysisPDEThe square-integrable space and the Sobolev space of the torus, with the Sobolev inner product, form a Hilbert triple satisfying the standing separability hypothesis; on twice continuously differentiable periodic functions its form operator is the identity minus the Laplacian.The Sobolev Space on the Torus is a Separable Hilbert Space Densely Embedded in the Square-Integrable Space
theoremthm:sobolev-h1-torus-2026aAnalysisPDEThe Sobolev space of once weakly differentiable square-integrable classes on the torus is complete, has a countable dense subset, contains the smooth periodic classes densely, and is itself dense in the square-integrable space. Mollification approximates a Sobolev class in the So…Linearity of the Lebesgue Integral over a Finite Sum of Integrable Functions
lemmalem:integral-finite-sum-2026aAnalysisA finite linear combination of integrable functions is integrable, and its integral is the corresponding linear combination of the integrals.The Sobolev Space of Once Weakly Differentiable Square-Integrable Classes on the Torus
definitiondef:sobolev-space-h1-torus-2026aAnalysisPDENames the space of square-integrable classes on the torus all of whose first weak partial derivatives are square-integrable, together with its inner product, norm and distance.Elementary Properties of the Weak Partial Derivative on the Torus
lemmalem:weak-derivative-torus-basic-2026aAnalysisPDEThe weak partial derivative extends the classical one on continuously differentiable periodic functions, is linear, may be tested against continuously differentiable periodic functions, commutes with mollification, is preserved by limits in the square-integrable space, and equips…- A function on the torus is an i-th weak partial derivative of another when integration against every smooth periodic test function obeys the integration-by-parts identity; the notion descends to almost-everywhere classes, where the weak derivative is unique.
Pairing an Integrable Function on the Torus with a Continuous Periodic Function
lemmalem:periodic-test-pairing-torus-2026aAnalysisThe product of an integrable function on the torus with a continuous periodic function is integrable, its integral is bounded by the supremum of the periodic factor times the integral of the absolute value of the other, and that integral is linear in each factor, depends only on…Transfer of a Partial Derivative in Periodic Convolution
lemmalem:periodic-convolution-derivative-torus-2026aAnalysisFor a smooth compactly supported kernel and a continuously differentiable periodic function, the derivative in a periodic convolution may be moved between the kernel and the function; consequently the mollifications of such a function converge to it uniformly together with their…The Lebesgue Bound for Periodic Convolution and Convergence of Mollifications
theoremthm:periodic-convolution-lp-torus-2026aAnalysisPeriodic convolution is bounded on every Lebesgue space of the torus by the mass of its kernel, the mollifications of a power-integrable function converge to it in that space, and the smooth periodic functions are dense there.- Wrapping a compactly supported kernel around the lattice gives a kernel that is continuous and periodic in each variable separately, as smooth as the original, has mass over the cell no larger than the original, is jointly measurable on the cell squared, and represents the period…
A Continuous Lattice-Periodic Function is Uniformly Continuous
lemmalem:continuous-periodic-uniformly-continuous-2026aAnalysisA continuous function that repeats over the integer lattice is uniformly continuous on the whole of Euclidean space, because it is determined by its values on a compact box.The Fundamental Lemma of the Calculus of Variations on the Torus
lemmalem:fundamental-lemma-torus-2026aAnalysisPDEA function integrable on the torus whose integral against every smooth periodic test function vanishes is zero almost everywhere.- Periodic convolution produces continuous periodic functions, is as smooth as its kernel with derivatives falling on the kernel, depends only on the class of the function, is linear in each argument, is bounded uniformly by a multiple of the seminorm of the function, and reproduce…
Periodic Convolution and Mollification on the Torus
definitiondef:periodic-convolution-torus-2026aAnalysisDefines the periodic convolution of a compactly supported continuous kernel with a power-integrable function on the torus, and the mollification obtained by taking the kernel to be a rescaled mollifier kernel.The Periodic Extension of a Function on the Unit Cell
lemmalem:periodic-extension-torus-2026aAnalysisWrapping a function on the unit cell around the lattice gives a periodic function on Euclidean space. The extension is measurable, linear, insensitive to changes on null sets, integrable on every bounded set, and has the same integral over every translate of the cell.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.Vanishing Mean of a Derivative and Integration by Parts on the Torus
lemmalem:periodic-integration-by-parts-2026aAnalysisPDEA partial derivative of a continuously differentiable periodic function has integral zero over the torus, so integration by parts on the torus carries no boundary term.