78 Boolean Analysis — Zk Fourier
78.1 Overview
This module develops the Fourier analysis of complex-valued functions on the domain \(\mathbb {Z}_k^n = (\mathbb {Z}/k\mathbb {Z})^n\), the natural generalization of the Boolean hypercube \(\{ 0,1\} ^n\). It establishes the primitive \(k\)-th root of unity \(\omega _k = e^{2\pi i/k}\), the associated group homomorphism \(a \mapsto \omega _k^a\), the Fourier characters \(\chi _s(x) = \omega _k^{s \cdot x}\), and the core identities: orthonormality of characters, the Fourier expansion, Parseval’s identity, and the convolution theorem.
78.2 Declarations
\(\texttt{ZkFourier.ZkVec}\ k\ n\) is the \(n\)-dimensional vector space over \(\mathbb {Z}/k\mathbb {Z}\), defined as the function type \(\mathrm{Fin}\, n \to \mathbb {Z}/k\mathbb {Z}\). It carries the pointwise additive group structure of \((\mathbb {Z}/k\mathbb {Z})^n\).
For \(k \geq 1\), the finite type \(\texttt{ZkFourier.ZkVec}\ k\ n\) has \(|\mathbb {Z}_k^n| = k^n\) elements.
\(\texttt{ZkFourier.rootOfUnity}\ k\) is the complex number \(\omega _k = e^{2\pi i / k}\), the primitive \(k\)-th root of unity used as the base of the Fourier characters on \(\mathbb {Z}_k^n\).
For \(a : \mathbb {Z}/k\mathbb {Z}\), \(\texttt{ZkFourier.toOmega}\ a = \omega _k^{a}\), where \(a\) is lifted to its canonical representative in \(\{ 0, \ldots , k-1\} \subset \mathbb {N}\). This is the group homomorphism \((\mathbb {Z}/k\mathbb {Z}, +) \to (\mathbb {C}^\times , \cdot )\).
\(\omega _k = e^{2\pi i/k}\) is a primitive \(k\)-th root of unity in \(\mathbb {C}\), i.e. \(\omega _k^k = 1\) and \(\omega _k^j \neq 1\) for \(0 \lt j \lt k\).
The \(k\)-th power of the root of unity satisfies \(\omega _k^k = 1\).
The embedding sends zero to one: \(\texttt{ZkFourier.toOmega}\ (0 : \mathbb {Z}/k\mathbb {Z}) = 1\).
For \(a, b : \mathbb {Z}/k\mathbb {Z}\), \(\omega _k^{a+b} = \omega _k^a \cdot \omega _k^b\). That is, \(\texttt{ZkFourier.toOmega}\) is a group homomorphism from \((\mathbb {Z}/k\mathbb {Z}, +)\) to \((\mathbb {C}^\times , \cdot )\).
For \(a : \mathbb {Z}/k\mathbb {Z}\), \(\omega _k^{-a} = \overline{\omega _k^a}\), i.e. \(\texttt{ZkFourier.toOmega}\ (-a) = \overline{\texttt{ZkFourier.toOmega}\ a}\).
For every \(a : \mathbb {Z}/k\mathbb {Z}\), \(\| \omega _k^a\| = 1\); the image of \(\texttt{ZkFourier.toOmega}\) lies on the complex unit circle.
For \(j, a : \mathbb {Z}/k\mathbb {Z}\), \(\omega _k^{j \cdot a} = (\omega _k^j)^a\), i.e. \(\texttt{ZkFourier.toOmega}\ (j \cdot a) = (\omega _k^{j.\mathrm{val}})^{a.\mathrm{val}}\).
For \(j : \mathbb {Z}/k\mathbb {Z}\),
This is the fundamental character-orthogonality identity for \(\mathbb {Z}/k\mathbb {Z}\).
\(\texttt{ZkFourier.ZkFun}\ k\ n\) is the type of complex-valued functions on \(\mathbb {Z}_k^n\), defined as \(\mathbb {Z}_k^n \to \mathbb {C}\). These are the objects whose Fourier transforms are studied.
The expectation of \(f : \mathbb {Z}_k^n \to \mathbb {C}\) is the uniform average
The Hermitian inner product of \(f, g : \mathbb {Z}_k^n \to \mathbb {C}\) is
The squared \(L^2\) norm of \(f : \mathbb {Z}_k^n \to \mathbb {C}\) is the real-valued quantity
The convolution of \(f, g : \mathbb {Z}_k^n \to \mathbb {C}\) is
For \(s, x \in \mathbb {Z}_k^n\), the dot product is \(s \cdot x = \sum _{i=0}^{n-1} s_i \, x_i \in \mathbb {Z}/k\mathbb {Z}\), computed componentwise modulo \(k\).
For \(s \in \mathbb {Z}_k^n\), the Fourier character indexed by \(s\) is \(\chi _s : \mathbb {Z}_k^n \to \mathbb {C}\) defined by \(\chi _s(x) = \omega _k^{s \cdot x}\). The \(k^n\) characters \(\{ \chi _s\} _{s \in \mathbb {Z}_k^n}\) form an orthonormal basis of \(L^2(\mathbb {Z}_k^n)\).
For \(s, x, y \in \mathbb {Z}_k^n\), \(s \cdot (x + y) = s \cdot x + s \cdot y\).
For any \(x \in \mathbb {Z}_k^n\), \(0 \cdot x = 0\).
For any \(s \in \mathbb {Z}_k^n\), \(s \cdot 0 = 0\).
For \(s, x \in \mathbb {Z}_k^n\), \((-s) \cdot x = -(s \cdot x)\).
For \(s, t, x \in \mathbb {Z}_k^n\), \((s - t) \cdot x = s \cdot x - t \cdot x\).
For \(s, x, y \in \mathbb {Z}_k^n\), \(\chi _s(x + y) = \chi _s(x) \cdot \chi _s(y)\). Each character is a group homomorphism from \((\mathbb {Z}_k^n, +)\) to \((\mathbb {C}^\times , \cdot )\).
For any \(s \in \mathbb {Z}_k^n\), \(\chi _s(0) = 1\).
For any \(x \in \mathbb {Z}_k^n\), \(\chi _0(x) = 1\); the character indexed by the zero frequency is identically one.
For all \(s, x \in \mathbb {Z}_k^n\), \(\| \chi _s(x)\| = 1\).
For all \(s, x \in \mathbb {Z}_k^n\), \(\chi _s(x) \neq 0\).
For \(s, x \in \mathbb {Z}_k^n\), \(\overline{\chi _s(x)} = \chi _{-s}(x)\). Complex conjugation of a character corresponds to negating its index.
For \(s, t, x \in \mathbb {Z}_k^n\), \(\chi _s(x) \cdot \chi _t(x) = \chi _{s+t}(x)\). Pointwise multiplication of characters corresponds to addition of their frequency indices.
If \(s \neq 0\), then \(\mathbb {E}[\chi _s] = 0\). This follows from the geometric sum identity: when some coordinate \(s_i \neq 0\), the sum over that coordinate vanishes.
\(\mathbb {E}[\chi _0] = 1\), since \(\chi _0 \equiv 1\) and the sum of \(k^n\) ones divided by \(k^n\) equals one.
For any \(s \in \mathbb {Z}_k^n\), \(\langle \chi _s, \chi _s \rangle = 1\). Every character is a unit-norm vector in \(L^2(\mathbb {Z}_k^n)\).
If \(s \neq t\), then \(\langle \chi _s, \chi _t \rangle = 0\). Together with \(\texttt{ZkFourier.inner\_ product\_ char\_ self}\), this shows that the characters form an orthonormal system.
The Fourier coefficient of \(f : \mathbb {Z}_k^n \to \mathbb {C}\) at frequency \(s\) is
For any \(s \in \mathbb {Z}_k^n\), \(\widehat{\chi _s}(s) = \langle \chi _s, \chi _s \rangle = 1\).
If \(s \neq t\), then \(\widehat{\chi _s}(t) = \langle \chi _s, \chi _t \rangle = 0\).
Every function \(f : \mathbb {Z}_k^n \to \mathbb {C}\) admits the Fourier expansion
The characters form a complete orthonormal basis of \(L^2(\mathbb {Z}_k^n)\).
For any \(f : \mathbb {Z}_k^n \to \mathbb {C}\),
Parseval’s identity expresses the conservation of \(L^2\) energy under the Fourier transform.
For \(f, g : \mathbb {Z}_k^n \to \mathbb {C}\) and \(s \in \mathbb {Z}_k^n\),
Convolution in the spatial domain corresponds to pointwise multiplication in the frequency domain.