OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterSums.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit modulus dependence in nonprincipal character partial sums, and the resulting exact Abel integral on its initial half-plane.

  1. lemma OAI.TwoPointCorrelations.mrt_character_shift line 14
  2. lemma OAI.TwoPointCorrelations.mrt_character_period_sum line 18
  3. lemma OAI.TwoPointCorrelations.mrt_character_full_periods line 34
  4. lemma OAI.TwoPointCorrelations.mrt_character_prefix_remainder line 44
  5. theorem OAI.TwoPointCorrelations.mrt_character_prefix_norm line 52
  6. lemma OAI.TwoPointCorrelations.mrt_character_Icc_eq line 62
  7. theorem OAI.TwoPointCorrelations.mrt_character_Icc_norm line 78
  8. lemma OAI.TwoPointCorrelations.mrt_character_sum_bigO line 84
  9. theorem OAI.TwoPointCorrelations.mrt_character_LFunction_Abel line 91