OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterAbel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Abel-integral bounds for every nonprincipal character, retaining the explicit modulus q in the bound q * norm(s) / re(s).

  1. def OAI.TwoPointCorrelations.mrtCharacterSummatory line 17
  2. def OAI.TwoPointCorrelations.mrtCharacterAbelKernel line 20
  3. def OAI.TwoPointCorrelations.mrtCharacterAbelIntegral line 23
  4. lemma OAI.TwoPointCorrelations.mrtCharacterSummatory_measurable line 27
  5. lemma OAI.TwoPointCorrelations.mrtCharacterSummatory_norm line 32
  6. lemma OAI.TwoPointCorrelations.mrtCharacterAbelKernel_measurable line 37
  7. lemma OAI.TwoPointCorrelations.mrtCharacterAbelKernel_norm_le line 46
  8. theorem OAI.TwoPointCorrelations.mrtCharacterAbelKernel_integrable line 55
  9. lemma OAI.TwoPointCorrelations.mrtCharacterAbelKernel_integral_norm line 64
  10. theorem OAI.TwoPointCorrelations.mrtCharacterAbelIntegral_norm line 79
  11. theorem OAI.TwoPointCorrelations.mrtCharacterAbelIntegral_eq_LFunction line 88