OAI/NumberTheory/JointDickman/Analysis/PrimeZetaLogReal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The real branch of the logarithmic Euler product

  1. theorem OAI.JointDickman.negative_real_log_im_zero line 8
  2. theorem OAI.JointDickman.primeZetaLog_im_eq_zero line 13
  3. theorem OAI.JointDickman.primeZetaLog_eq_log line 28
  4. theorem OAI.JointDickman.squarefreeDirichletSeries_real_factorization line 38