English
Define the discrete Fourier transform on the finite cyclic group ZMod N with values in E, as a linear equivalence 𝓕 between functions ZMod N → E and itself, using the standard additive character.
Русский
Определяем дискретное преобразование Фурье на ZMod N как линейное эквивалентность 𝓕 между функциями ZMod N → E, через стандартный аддитивный характер.
LaTeX
$$$\\mathcal{F} : (\\mathbb{Z}/N\\mathbb{Z} \\to E) \\to (\\mathbb{Z}/N\\mathbb{Z} \\to E)$ is a ℂ-linear isomorphism with explicit formula $ (\\mathcal{F} \\Phi)(k) = \\sum_{j \\in \\mathbb{Z}/N\\mathbb{Z}} \\mathrm{stdAddChar}(-jk) \\cdot \\Phi(j).$$$
Lean4
/-- The discrete Fourier transform on `ℤ / N ℤ` (with the counting measure), bundled as a linear
equivalence. Denoted as `𝓕` within the `ZMod` namespace.
-/
noncomputable def dft : (ZMod N → E) ≃ₗ[ℂ] (ZMod N → E)
where
toFun := auxDFT
map_add' Φ₁ Φ₂ := by ext; simp only [auxDFT, Pi.add_def, smul_add, sum_add_distrib]
map_smul' c Φ := by ext; simp only [auxDFT, Pi.smul_apply, RingHom.id_apply, smul_sum, smul_comm c]
invFun Φ k := (N : ℂ)⁻¹ • auxDFT Φ (-k)
left_inv Φ := by simp only [auxDFT_auxDFT, neg_neg, ← mul_smul, inv_mul_cancel₀ (NeZero.ne _), one_smul]
right_inv
Φ := by
ext1 j
simp only [← Pi.smul_def, auxDFT_smul, auxDFT_neg, auxDFT_auxDFT, neg_neg, ← mul_smul,
inv_mul_cancel₀ (NeZero.ne _), one_smul]
