OAI/NumberTheory/CubicMoment/Estimates/IdealLogDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic derivative of the complete ideal series is the actual ideal von Mangoldt Dirichlet series on Re(s)>1.

  1. lemma OAI.CubicFirstMoment.idealVonMangoldt_antidiagonal line 13
  2. lemma OAI.CubicFirstMoment.idealVonMangoldt_twist_convolution line 21
  3. lemma OAI.CubicFirstMoment.idealVonMangoldt_tsum_mul line 37
  4. theorem OAI.CubicFirstMoment.idealDirichlet_neg_logDeriv line 49