OAI/NumberTheory/Ostmann/Characters/PeriodicPolynomialCharacterSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.periodic_polynomial_integer_character_sum line 13

   Source documentation

   A bounded function of the residue modulo the frequency modulus is constant on each progression. It therefore retains the same cancellation bound.

   theorem periodic_polynomial_integer_character_sum {q r : ℕ} [NeZero q] [NeZero r]
       (hqr : q.Coprime r) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r)
       (hχ : χ ≠ 1) (a Q K : ℕ) (ha : 0 < a) (hQ : Q.Coprime (q * r))
       {n t : ℕ} (F : Fin n → ClippedPolynomialFactor) (H : Fin t → Polynomial ℝ)
       (keep : (Fin t → Bool) → Bool) (gate : ZMod Q → ℂ) (hgate : ∀ z, ‖gate z‖ ≤ 1) :
       ‖∑ j : Fin (K * Q), gate ((a + j.val : ℕ) : ZMod Q) *
         supportedPolynomialWeight F H keep ((a + j.val : ℕ) : ℝ) *
         (χ ((a + j.val : ℕ) : ZMod q) * conj (ψ ((a + j.val : ℕ) : ZMod r)))‖ ≤
         (Q : ℝ) * ((3 ^ ((∑ i, (F i).polynomial.derivative.natDegree) +
           ∑ i, (H i).natDegree) : ℕ) *
           (2 * (a : ℝ)⁻¹ * smoothPolynomialBudget F) * (q * r)) := by
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.supportedPolynomialWeight, OAI.Ostmann.smoothPolynomialBudget