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