fourierTransform_eq_gaussSum_mulShift

English

For a Dirichlet character χ, the Fourier transform satisfies 𝓕 χ(k) = gaussSum χ(stdAddChar.mulShift(-k)).

Русский

Для персона Dirichlet χ Фурье-преобразование удовлетворяет 𝓕 χ(k) = gaussSum χ(stdAddChar.mulShift(-k)).

LaTeX

$$$\\\\mathcal{F} \\\\chi(k) = gaussSum \\\\chi (stdAddChar.mulShift(-k))$$$

Lean4

theorem fourierTransform_eq_gaussSum_mulShift (χ : DirichletCharacter ℂ N) (k : ZMod N) :
    𝓕 χ k = gaussSum χ (stdAddChar.mulShift (-k)) :=
  by
  simp only [dft_apply, smul_eq_mul]
  congr 1 with j
  rw [mulShift_apply, mul_comm j, neg_mul, stdAddChar_apply, mul_comm (χ _)]

Похожие утверждения