OAI/NumberTheory/JointDickman/Analysis/SquarefreeCharacterFactorization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Analytic factorization of the twisted squarefree Dirichlet series

  1. def OAI.JointDickman.primeCharacterLog line 9
  2. theorem OAI.JointDickman.primeCharacterLog_summable line 12
  3. theorem OAI.JointDickman.primeCharacterLog_exp line 17
  4. theorem OAI.JointDickman.primeCharacterLog_summand_bound line 22
  5. theorem OAI.JointDickman.primeCharacterLog_differentiableOn line 41
  6. theorem OAI.JointDickman.primeCharacterLog_analyticOnNhd line 62
  7. theorem OAI.JointDickman.squarefreeCharacterDirichletSeries_factorization line 70