OAI/NumberTheory/Ostmann/Characters/QuartetFourier.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fourier estimates for quartet terms

The friendly term follows from the uniform Mellin estimate and Parseval energy. A nonprincipal Gauss transform also has the uniform maximum used when exactly one of the two quartet twists is principal.

  1. theorem OAI.Ostmann.weightedCharacterSum_norm_le line 22
  2. theorem OAI.Ostmann.nonprincipal_fourier_norm_sq_le line 35
  3. theorem OAI.Ostmann.friendly_fourier_sum_le line 51

    Source documentation

    The friendly convolution sum uses one uniform Mellin bound and one total energy.

    theorem friendly_fourier_sum_le {p : ℕ} [Fact p.Prime]
    (P Q : MulChar (ZMod p) ℂ → ZMod p → ℂ)
    (δ C : ℝ) (hδ : 0 ≤ δ)
    (hP : ∀ (η : MulChar (ZMod p) ℂ) (a : ZMod p),
      (∑ χ : MulChar (ZMod p) ℂ,
        ‖additiveFourier (fun x => P χ x * χ x * η x) a‖ ^ 2) ≤ δ)
    (hQ : (∑ ψ : MulChar (ZMod p) ℂ, ∑ a : ZMod p, ‖additiveFourier (Q ψ) a‖ ^ 2) ≤ C)
    (η : MulChar (ZMod p) ℂ → MulChar (ZMod p) ℂ) :
    (∑ a : ZMod p, ∑ ψ : MulChar (ZMod p) ℂ, ∑ χ : MulChar (ZMod p) ℂ,
      ‖additiveFourier (fun x => P χ x * χ x * η ψ x) a‖ ^ 2 *
        ‖additiveFourier (Q ψ) (-a)‖ ^ 2) ≤ δ * C := by
…

    Mentions: OAI.Ostmann.additiveFourier