TranslatedCharacterPoisson.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The translated primitive-character Poisson identity

This is the exact finite-modulus transform used before the squarefree frequency decomposition in Section 3 of the manuscript.

theorem OAI.Ostmann.translated_character_crt_fourier line 16
theorem OAI.Ostmann.quadratic_character_inverse_value line 35

theorem OAI.Ostmann.quadratic_translated_crt_fourier line 45

Source documentation

For a quadratic character, the inverse frequency multiplier contributes the ordinary character value of the other coprime modulus.

theorem quadratic_translated_crt_fourier {d M : ℕ} [NeZero d] [NeZero M]
    (h : d.Coprime M) (f : ZMod d → ℂ) (χ : DirichletCharacter ℂ M)
    (hχ : χ.IsPrimitive) (hq : χ.IsQuadratic) (t : ZMod M) (u : ZMod (d * M)) :
    additiveFourier (fun x => f ((ZMod.chineseRemainder h) x).1 *
      χ (((ZMod.chineseRemainder h) x).2 - t)) (-u) =
      additiveFourier f (-((M : ZMod d)⁻¹ * ((ZMod.chineseRemainder h) u).1)) *
      ZMod.stdAddChar (t * ((d : ZMod M)⁻¹ * ((ZMod.chineseRemainder h) u).2)) *
      (M : ℂ)⁻¹ * χ (d : ZMod M) * χ ((ZMod.chineseRemainder h) u).2 *
      gaussSum χ ZMod.stdAddChar := by
…

Mentions: OAI.Ostmann.additiveFourier

theorem OAI.Ostmann.quadratic_character_poisson line 58