OAI/NumberTheory/JointDickman/Analysis/SquarefreeEulerAnalytic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The analytic Euler correction in the half-plane Re(s) > 1/2

  1. def OAI.JointDickman.squarefreePrimeLog line 12
  2. def OAI.JointDickman.squarefreeLogFactor line 15
  3. def OAI.JointDickman.squarefreeAnalyticFactor line 18
  4. theorem OAI.JointDickman.prime_negative_cpow_norm_le line 21
  5. theorem OAI.JointDickman.squarefreePrimeLog_uniform_bound line 30
  6. theorem OAI.JointDickman.squarefreePrimeLog_bound_summable line 49
  7. theorem OAI.JointDickman.squarefreePrimeLog_summable line 54
  8. theorem OAI.JointDickman.squarefreePrimeLog_differentiableAt line 60
  9. theorem OAI.JointDickman.squarefreeLogFactor_differentiableOn line 80
  10. theorem OAI.JointDickman.squarefreeLogFactor_analyticOnNhd line 89
  11. theorem OAI.JointDickman.squarefreeAnalyticFactor_analyticOnNhd line 98
  12. theorem OAI.JointDickman.squarefreeAnalyticFactor_ne_zero line 102