English
Explicit formula for the L-function of the discrete Fourier transform: LFunction(𝓕Φ) s equals the finite sum over residues j of Φ(j) times expZeta(-j) on the circle.
Русский
Явная формула для L-функции дискретного преобразования Фурье: LFunction(𝓕Φ) s равна конечной сумме по j от Φ(j)·expZeta(-j) на окружности.
LaTeX
$$$$L(\mathcal{F}\Phi, s) = \sum_{j \in \mathbb{Z}/N\mathbb{Z}} \Phi(j) \expZeta( -j )(s).$$$$
Lean4
/-- Explicit formula for the L-function of `𝓕 Φ`, where `𝓕` is the discrete Fourier transform. -/
theorem LFunction_dft (Φ : ZMod N → ℂ) {s : ℂ} (hs : Φ 0 = 0 ∨ s ≠ 1) :
LFunction (𝓕 Φ) s = ∑ j : ZMod N, Φ j * expZeta (toAddCircle (-j)) s :=
by
have (j : ZMod N) : Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s :=
by
by_cases h : -j ≠ 0 ∨ s ≠ 1
· rw [LFunction_stdAddChar_eq_expZeta _ _ h]
· simp only [neg_ne_zero, not_or, not_not] at h
rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
simp only [LFunction, ← this, mul_sum]
rw [dft_def, sum_comm]
simp only [sum_mul, mul_sum, smul_eq_mul, stdAddChar_apply, ← mul_assoc]
congr 1 with j
congr 1 with k
rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]
