Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Step functions taking rational values on the dyadic subcubes of the unit cube form a countable dense family, so every Lebesgue space of the torus is separable.
Continuous Periodic Functions are Power-Integrable and Dense on the Torus
lemmalem:continuous-periodic-dense-lp-torus-2026aAnalysisRestricting a continuous periodic function to the unit cube gives an element of every Lebesgue space of the torus, linearly in the function, and these elements are dense there.- Standing notation for analysis on the flat torus: the half-open unit cube with the restriction of Lebesgue measure, the resulting Lebesgue spaces, the periodic function classes, and the gradient and Laplacian.
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.- The classes of power-integrable simple functions form a dense linear subspace of the Lebesgue space.
The Lebesgue Space of Square-Integrable Functions is a Real Hilbert Space
lemmalem:l2-real-hilbert-space-2026aAnalysisFor exponent two the Lebesgue space carries an inner product given by the integral of the product, whose norm is the two-norm, and it is a real Hilbert space.The Riesz-Fischer Theorem: the Lebesgue Space is a Real Banach Space
theoremthm:riesz-fischer-lp-2026aAnalysisThe Lebesgue space of power-integrable functions is a real Banach space, and a norm-convergent sequence has a subsequence converging almost everywhere with a single power-integrable dominating function.- Defines the Lebesgue space as the set of classes of power-integrable functions that agree almost everywhere, with the induced operations and norm.
- Defines a norm on a real vector space, the metric it induces, the topological vocabulary read in that metric, and completeness, which makes the space a real Banach space.
Minkowski's Inequality and the Seminormed Space of Power-Integrable Functions
lemmalem:minkowski-inequality-2026aAnalysisThe p-seminorm of a sum is at most the sum of the seminorms, so the power-integrable functions form a real vector space on which the p-seminorm is subadditive and absolutely homogeneous.- The integral of a product of power-integrable functions is bounded by the product of their seminorms, both for a conjugate pair of exponents and for finitely many exponents whose reciprocals sum to one.
- The p-seminorm is absolutely homogeneous, respects almost-everywhere comparison, vanishes exactly on functions that are zero almost everywhere, and rescales under powers of the integrand.
- Defines the set of measurable real-valued functions whose p-th power has finite integral, and the p-seminorm of such a function.
Approximation of Measurable Functions by Simple Functions
lemmalem:simple-function-approximation-2026aAnalysisEvery nonnegative measurable function is the pointwise supremum of a nondecreasing sequence of nonnegative simple functions, and every measurable real-valued function is a pointwise limit of simple functions dominated by its absolute value.The Lebesgue Integral and Null Sets: Almost-Everywhere Comparison, Markov's Inequality, and Dominated Convergence Almost Everywhere
lemmalem:integral-almost-everywhere-2026aAnalysisCountable unions of null sets are null; integrals ignore null sets; a nonnegative integral vanishes exactly when the integrand vanishes almost everywhere; Markov's inequality; and dominated convergence under almost-everywhere hypotheses.Conjugate Exponents and Young's Inequality
lemmalem:young-inequality-conjugate-exponents-2026aAnalysisEvery exponent larger than one has a unique conjugate, and a product of two nonnegative numbers is bounded by the sum of their powers divided by the conjugate exponents.Measure Spaces and the Lebesgue Integral: Standing Notation
settingset:measure-space-integration-2026aAnalysisStanding notation for a measure space, measurable and simple functions, the Lebesgue integral, null sets and almost-everywhere statements, and powers with nonnegative base, together with the background results in force.Properties of Real Powers of Nonnegative Real Numbers
lemmalem:nonnegative-real-power-properties-2026aAnalysisCollects the algebraic and order properties of the power map on the nonnegative half-line: multiplicativity, the exponent laws, strict monotonicity, continuity, and the inverse power map.