OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeEulerProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the squarefree Selberg–Delange Euler factor

Cancellation of the linear local logarithms proves absolute convergence. This identifies the same Euler product used in the published leading coefficient, without assuming its convergence as another input.

  1. def OAI.JointDickman.squarefreeEulerFactor line 22
  2. def OAI.JointDickman.primeEulerFactor line 25
  3. theorem OAI.JointDickman.log_one_add_sub_error line 28
  4. theorem OAI.JointDickman.squarefreeEulerFactor_pos line 38
  5. theorem OAI.JointDickman.squarefreeEulerFactor_log_bound line 49
  6. theorem OAI.JointDickman.primeEulerFactor_pos line 81
  7. theorem OAI.JointDickman.primeEulerFactor_log_summable line 87
  8. theorem OAI.JointDickman.primeEulerFactor_multipliable line 98
  9. theorem OAI.JointDickman.squarefreeEulerProduct_pos line 102
  10. theorem OAI.JointDickman.squarefreeEulerProduct_eq line 107
  11. theorem OAI.JointDickman.squarefreeEulerProduct_partial line 117
  12. theorem OAI.JointDickman.squarefreeEulerProduct_partial_tendsto line 131