English
For Φ: ZMod N → ℂ, the DFT is even if and only if Φ is even: (𝓕Φ) is even ⇔ Φ is even.
Русский
Для Φ: ZMod N → ℂ преобразование Фурье четно тогда и только тогда, когда сама функция Φ четна.
LaTeX
$$$((\\\\mathcal{F}\\\\Phi).\\\\Even) \\iff (\\\\Phi).\\\\Even$$$
Lean4
/-- The discrete Fourier transform of `Φ` is even if and only if `Φ` itself is. -/
theorem dft_even_iff {Φ : ZMod N → ℂ} : (𝓕 Φ).Even ↔ Φ.Even :=
by
have h {f : ZMod N → ℂ} (hf : f.Even) : (𝓕 f).Even := by
simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]
refine ⟨fun hΦ x ↦ ?_, h⟩
simpa only [neg_neg, smul_right_inj (NeZero.ne (N : ℂ)), dft_dft] using h hΦ (-x)
