PolynomialCharacterSum.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Character cancellation for the actual smooth polynomial weight

The interval and variation hypotheses are constructed from the polynomial roots. Only a bounded function of the root cell is retained for the regular supports. Irregular unary prime restrictions are handled separately by Cauchy--Schwarz.

theorem OAI.Ostmann.polynomial_weighted_character_progression line 18

Source documentation

One allowed residue progression. The factor 1/a is the long-variable saving; summing over the residue classes gives the frequency-modulus loss.

theorem polynomial_weighted_character_progression {q r : ℕ} [NeZero q] [NeZero r]
    (hqr : q.Coprime r) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r)
    (hχ : χ ≠ 1) (a M N : ℕ) (ha : 0 < a) (hM : M.Coprime (q * r))
    {n : ℕ} (F : Fin n → ClippedPolynomialFactor) (S : Finset ℝ)
    (hroots : ∀ i x, x ∈ (F i).polynomial.derivative.roots → x ∈ S)
    (flag : (S → Ordering) → ℂ) (hflag : ∀ i, ‖flag i‖ ≤ 1) :
    ‖∑ j ∈ Finset.range N,
      flag (rootCellCode S ((a + M * j : ℕ) : ℝ)) *
      (Complex.ofReal (((a + M * j : ℕ) : ℝ)⁻¹) *
        smoothPolynomialWeight F ((a + M * j : ℕ) : ℝ)) *
      (χ ((a + M * j : ℕ) : ZMod q) * conj (ψ ((a + M * j : ℕ) : ZMod r)))‖ ≤
      (3 ^ S.card : ℕ) * (2 * (a : ℝ)⁻¹ * smoothPolynomialBudget F) * (q * r) := by
…

Mentions: OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.rootCellCode, OAI.Ostmann.smoothPolynomialWeight, OAI.Ostmann.smoothPolynomialBudget