How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Fourier coefficients and trigonometric polynomials on the torus
Definition
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()) and let with its normalized Haar integral (The one-dimensional torus and its normalized Haar integral).
Characters. For define by for , where is the complex exponential (The complex exponential by its power series). The definition is independent of the representative : replacing by with adds the period to the argument of sine and cosine. Each is continuous, hence Borel, and satisfies
the last two by the cartesian form of , , and and Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive. In particular and every is bounded and nonzero everywhere.
Fourier coefficients. Let (Complex Lp classes and Euclidean test-function conventions), that is, a class of Borel functions with . Define the Fourier coefficient of at by
This is well defined: because , so and its integral is finite; and the integral depends only on the class of , because it is unchanged when is modified on a null set (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree). The map is complex-linear for each (The Lebesgue integral is linear on ).
Trigonometric polynomials. A trigonometric polynomial on is a finite complex linear combination of characters, , for a finite and scalars . The set of all trigonometric polynomials is the span of ; it is closed under addition, scalar multiplication, multiplication and complex conjugation (by the identities for and ), and it contains . Nothing is claimed here about uniqueness of the coefficients in an expansion, nor about the size of ; those are properties of the characters proved below.
The finite torus. On , , the characters are for , where is the Euclidean dot product of a representative tuple; trigonometric polynomials are finite complex linear combinations of these, and Fourier coefficients of are . Fubini computes integrals of products of characters on the product measure (Fubini's theorem for L^1 functions on a sigma-finite product); for Hölder's inequality makes integrable (Complex Holder, Minkowski, and the quotient norm, Finite-measure includes into for ).
Depends on
- The one-dimensional torus and its normalized Haar integral
- Finite-measure $L^r$ includes into $L^p$ for $p < r$
- The complex exponential by its power series
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Complex Lp classes and Euclidean test-function conventions
- Complex Holder, Minkowski, and the quotient norm
- Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree
- The Lebesgue integral is linear on $L^1(\mu)$
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- Fubini's theorem for L^1 functions on a sigma-finite product
Used by
- Trigonometric polynomials are uniformly dense in continuous functions on the torus Corollary
- The Fourier series of a sawtooth and the Basel sum Example
- The Fourier series of a square wave and the odd reciprocal-square sum Example
- The trigonometric characters are orthonormal in L² of the torus Lemma
- Fourier series converge in mean square Theorem
- Riesz–Fischer: the Fourier coefficient map is onto the space of square-summable families Theorem
- The Fourier basis and Parseval's identity on the finite torus Theorem
- The Parseval identity for Fourier series Theorem
- The trigonometric system is complete in L² of the torus Theorem
Dependency tree · two levels
100 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.5, pp.63–64, equations (2.42)–(2.44) (standard reference, not scraped)
- Theo Bühler and Dietmar Salamon, Functional Analysis — Example 2.66, pp.87–88 (standard reference, not scraped)