fourierTransform_eq_inv_mul_gaussSum

English

For a primitive Dirichlet character χ, 𝓕 χ(k) = χ⁻¹(-k) · gaussSum χ(stdAddChar).

Русский

Для примитивного Dirichlet χ, 𝓕 χ(k) = χ⁻¹(-k) \\, gaussSum χ(stdAddChar).

LaTeX

$$$\\\\mathcal{F} χ(k) = χ^{-1}(-k) \\\\cdot gaussSum χ stdAddChar$$$

Lean4

/-- For a primitive Dirichlet character `χ`, the Fourier transform of `χ` is a constant multiple
of `χ⁻¹` (and the constant is essentially the Gauss sum). -/
theorem fourierTransform_eq_inv_mul_gaussSum {χ : DirichletCharacter ℂ N} (hχ : IsPrimitive χ) (k : ZMod N) :
    𝓕 χ k = χ⁻¹ (-k) * gaussSum χ stdAddChar := by
  rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]

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