Properties of the Fourier Coefficients on the Torus, and the Realisation of Weighted Coefficient Families
lemmaAnalysislem:fourier-coefficients-torus-2026aThe Fourier coefficient map is linear and injective, Parseval's identity and the Fourier expansion hold along any enumeration of the lattice, a square-summable coefficient family along an enumeration comes from exactly one class, and for each natural number m the families whose rescaling by the m-th power of the inverse square roots of the Fourier weights come from a class form a linear subspace of the coefficient families on which the realisation is a linear bijection onto the square-integrable classes.
We work in the setting of The Flat Torus: Standing Notation, used here with a natural number satisfying , and in the setting of Real Hilbert Spaces: Standing Notation and Background, whose standing space is not used here; the integer lattice , Euclidean space with its norm , and the real Hilbert space are the ones fixed there, with inner product and norm and zero vector . Let for be the classes of the trigonometric system introduced in The Trigonometric System on the Torus is Orthonormal §classes, and for let be its Fourier coefficient family, an element of the set of all maps from to , which is a real vector space under the pointwise operations, with zero vector the zero family, the map with value everywhere; its elements are called coefficient families. A bijection is called an enumeration of the lattice; one exists by The Integer Lattice Admits an Enumeration by the Natural Numbers §enumeration. Series of real numbers and series in and their sums are as defined there. Powers of a real number with are natural powers; in particular , with , by claim 1 of Properties of Natural Number Powers in a Field.
Let for be the Fourier weights fixed there, that lemma being used with ; they are positive by Summability of the Negative Powers of the Fourier Weights of the Torus §product, so that is positive by claim 7 of Elementary Order Arithmetic in an Ordered Field. For let be the nonnegative real number with furnished by Existence and Uniqueness of the Nonnegative Square Root; it is nonzero, since by claim 1 of Zero Products and Elementary Identities in a Field, hence positive. Then the following hold.
1. (Linearity)¶ For all and , and ; that is, the map from to is linear.
2. (Injectivity)¶ If satisfy , then .
3. (The trigonometric classes)¶ For , equals if and equals if .
4. (Parseval's identity and the Fourier expansion)¶ Let be an enumeration and . Then the series converges with sum , in particular
and the series converges in with sum .
5. (Square-summable families are Fourier coefficient families)¶ Let be an enumeration and let be such that the series converges. Then there is exactly one with ; it is the sum of the series , which converges in , and .
6. (Realisation of weighted coefficient families)¶ Let , and let be the set of those for which there is with
Then for every there is exactly one such , written ; the set is a linear subspace of , hence a real vector space under the pointwise operations; and the map is linear and a bijection.
Loading…
Prerequisites
No prerequisites tracked.
Dependents
No dependents yet.
Dependent proofs
No dependent proofs yet.
No relations recorded yet.