OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterLogGrowth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One absolute constant in the nonprincipal disk bounds, with all modulus and height dependence kept in log(q*(abs(t)+2)).

  1. def OAI.TwoPointCorrelations.mrtCharacterHeight line 10
  2. lemma OAI.TwoPointCorrelations.mrt_character_height_split line 13
  3. lemma OAI.TwoPointCorrelations.mrt_character_height_ge line 17
  4. lemma OAI.TwoPointCorrelations.mrt_character_height_pos line 23
  5. lemma OAI.TwoPointCorrelations.mrt_character_log_modulus_le_height line 28
  6. lemma OAI.TwoPointCorrelations.mrt_character_height_double line 33
  7. lemma OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant_pos line 47
  8. lemma OAI.TwoPointCorrelations.mrt_character_log_disk_growth line 52
  9. theorem OAI.TwoPointCorrelations.mrt_character_logderiv_growth_constant line 86