OAI/NumberTheory/Ostmann/Characters/PeriodicCharacterSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Initial sums of nonprincipal periodic characters

  1. theorem OAI.Ostmann.sum_range_periodic_blocks line 11
  2. theorem OAI.Ostmann.periodic_zero_sum_range_bound line 21
  3. theorem OAI.Ostmann.nonprincipal_character_sum_range_bound line 32
  4. theorem OAI.Ostmann.nonsquare_jacobi_sum_range_bound line 55

    Source documentation

    The nonsquare term in the original odd-modulus Jacobi moment has a uniform initial-sum bound, with no analytic hypothesis.

    theorem nonsquare_jacobi_sum_range_bound (n N : ℕ) (hn : 0 < n)
    (hns : ¬IsSquare n) :
    |∑ a ∈ Finset.range N, if Odd a then realJacobi n a else 0| ≤ 8 * n := by
…

    Mentions: OAI.Ostmann.realJacobi