OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDirichlet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact prime-power separation of the original arithmetic Dirichlet series. Absolute convergence is used only for the iterated sum.

  1. def OAI.CubicFirstMoment.cubicThetaDenominatorTerm line 12
  2. def OAI.CubicFirstMoment.cubicThetaPrimePowerTerm line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_denominators line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaDenominatorTerm_summable line 35
  5. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primePowers line 46
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_summable line 53
  7. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primePowers_iterated line 58
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_high line 65
  9. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_two_terms line 74