OAI/NumberTheory/Ostmann/Characters/PrimitiveGaussFourier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact primitive-character Fourier transform at composite modulus

This supplies the complete transform and Gauss normalization needed in the quadratic Poisson step, using the proved library character identities.

  1. theorem OAI.Ostmann.primitive_character_fourier line 17
  2. theorem OAI.Ostmann.primitive_gauss_norm_sq line 32

    Source documentation

    Parseval gives the primitive Gauss-sum norm without a prime-modulus restriction and without assuming a separate analytic input.

    theorem primitive_gauss_norm_sq {N : ℕ} [NeZero N]
    (χ : DirichletCharacter ℂ N) (hχ : χ.IsPrimitive) :
    ‖gaussSum χ (ZMod.stdAddChar (N := N))‖ ^ 2 = (N : ℝ) := by
…