PolynomialIntegerCharacterSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the residue classes of the long-integer interval

def OAI.Ostmann.supportedPolynomialWeight line 11

theorem OAI.Ostmann.supported_polynomial_integer_character_sum line 18

Source documentation

This is the bound after summing all frequency-modulus residue classes. No integer endpoint is removed in the exact rectangular interval.

theorem supported_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) :
    ‖∑ j : Fin (K * 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