OAI/NumberTheory/Ostmann/Characters/NormalizedMixedFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Mixed Fourier coefficients of the normalized residue transform

The principal coefficient is controlled by Fourier inversion. Nonprincipal coefficients are exactly the translated residue bias times its density factor.

  1. theorem OAI.Ostmann.additiveFourier_densityFourier line 17
  2. theorem OAI.Ostmann.normalizedResidueTransform_principal line 25
  3. theorem OAI.Ostmann.densityFourier_mixed_character line 44
  4. theorem OAI.Ostmann.normalizedResidueIndicator_character_sum line 64
  5. theorem OAI.Ostmann.normalizedResidueTransform_nonprincipal line 86
  6. theorem OAI.Ostmann.normalizedResidueTransform_mixedBound line 111

    Source documentation

    The exact Gauss identity supplies the local mixed bound used by the tree comparison once the translated character means have been bounded.

    theorem normalizedResidueTransform_mixedBound {p : ℕ} [Fact p.Prime]
    (S : Finset (ZMod p)) (hlo : (1 / 3 : ℝ) ≤ residueDensity S)
    (hhi : residueDensity S ≤ 2 / 3) (β : ℝ)
    (hbias : ∀ (χ : MulChar (ZMod p) ℂ), χ ≠ 1 → ∀ a : ZMod p,
      ‖(S.card : ℂ)⁻¹ * ∑ x ∈ S, χ⁻¹ (-a - x)‖ ≤ β) :
    MixedFourierBound (normalizedResidueTransform S)
      (max (3 / Real.sqrt (p : ℝ)) (2 * β)) := by
…

    Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.MixedFourierBound, OAI.Ostmann.normalizedResidueTransform