OAI/NumberTheory/JointDickman/Analysis/SquarefreeCharacterEuler.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The absolutely convergent Euler correction for squarefree character sums

  1. def OAI.JointDickman.characterPrimePower line 10
  2. def OAI.JointDickman.squarefreeCharacterPrimeLog line 13
  3. def OAI.JointDickman.squarefreeCharacterLogFactor line 17
  4. def OAI.JointDickman.squarefreeCharacterAnalyticFactor line 20
  5. theorem OAI.JointDickman.characterPrimePower_norm_le line 23
  6. theorem OAI.JointDickman.squarefreeCharacterPrimeLog_bound line 29
  7. theorem OAI.JointDickman.squarefreeCharacterPrimeLog_summable line 56
  8. theorem OAI.JointDickman.squarefreeCharacterPrimeLog_differentiableAt line 64
  9. theorem OAI.JointDickman.squarefreeCharacterLogFactor_differentiableOn line 85
  10. theorem OAI.JointDickman.squarefreeCharacterLogFactor_analyticOnNhd line 97
  11. theorem OAI.JointDickman.squarefreeCharacterAnalyticFactor_analyticOnNhd line 109
  12. theorem OAI.JointDickman.squarefreeCharacterAnalyticFactor_uniform_bound line 114