Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Trigonometric System is Continuously Differentiable and Orthogonal in the Sobolev Space of the Torus
lemmalem:trigonometric-system-sobolev-torus-2026aAnalysisPDEEach member of the trigonometric system is continuously differentiable and periodic, with partial derivatives again members of the system up to a factor; its classes therefore lie in the Sobolev space of the torus and are orthogonal there, with squared norm one plus four pi squar…The Lebesgue Space of Square-Integrable Functions on the Torus is Not Finite-Dimensional
corollarycor:l2-torus-not-finite-dimensional-2026aAnalysisThe classes of the trigonometric system indexed along a single coordinate axis form an orthonormal sequence, so the Lebesgue space of square-integrable functions on the torus is not finite-dimensional.The Trigonometric System on the Torus is Orthonormal
theoremthm:trigonometric-system-orthonormal-torus-2026aAnalysisEach member of the trigonometric system is continuous and periodic, so defines a class in the Lebesgue space of square-integrable functions on the torus; these classes form an orthonormal family indexed by the integer lattice.- The real trigonometric system on the flat torus, indexed by the integer lattice: a normalised cosine or sine in each coordinate according to the sign of the index, multiplied together.
- The functions and for integer : their derivatives and bounds, and the values of the integrals over the half-open unit interval of each of them and of each pairwise product.
Zero Extension of a Real-Valued Function, and the Unit-Cell Integral of a Continuous Function
lemmalem:zero-extension-cell-integral-2026aAnalysisA real-valued function on a measurable subset is measurable and integrable exactly when its zero extension is, with the same integral; consequently the integral over the half-open unit interval of a continuous function is its Riemann integral over the closed one.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.Quarter-Turn Identities and Periodicity of Sine and Cosine
theoremthm:sine-cosine-periodicity-2026bAnalysisThe values of sine and cosine at π/2 and π; shifting the argument by π/2 exchanges the sine and the cosine up to sign, and iterating gives the half-turn identities and invariance under every integer multiple of 2π. The sine is positive on (0, π).- is twice the least positive zero of the cosine.
- There is exactly one positive real number at which the cosine vanishes and before which it is positive; it is less than 2, and the sine is positive up to it and equals 1 there.
- Each of the sums and equals twice one of the products , , .
- The cosine and sine of a sum expand as and .
- The sum of the squares of the cosine and the sine is everywhere; consequently both functions are bounded in absolute value by .
Continuity, Derivatives and Power Series of Sine and Cosine
theoremthm:sine-cosine-calculus-2026bAnalysisThe real sine and cosine are continuous and differentiable on the real line, with derivatives cos and -sin. Their Maclaurin series converge absolutely to them.- The factorial satisfies and for every natural number .
- Defines the real cosine and sine as the real and imaginary parts of the complex exponential on the imaginary axis.
Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials
lemmalem:factorial-power-series-majorant-2026aAnalysisFactorials are positive and nondecreasing, the series of powers of a nonnegative real number divided by factorials converges, and it dominates the two series of even and odd order that define cosine and sine.Differentiability at an Interior Point is a Local Property
lemmalem:derivative-local-interval-2026aAnalysisIf a real function restricted to a subinterval containing a neighbourhood of an interior point is differentiable there, then the function itself is differentiable at that point, with the same derivative.- A series of real numbers converges exactly when the series of its terms from the second onward converges, and then its sum is the first term plus that sum.
Series of Real-Valued Functions and Their Partial Sums
definitiondef:series-of-functions-2026aAnalysisDefines the partial sums of a sequence of real-valued functions on a set, and pointwise and uniform convergence of the resulting series on a subset of that set.