OAI/NumberTheory/CubicMoment/Estimates/SquarefreeThirdMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The third divisor moment on primary squarefree elements, from a finite Euler product and the already specified ordinary prime theorem.

  1. lemma OAI.CubicFirstMoment.squarefree_eight_reciprocal_sum line 12
  2. lemma OAI.CubicFirstMoment.squarefree_eight_sum_le_euler line 35
  3. theorem OAI.CubicFirstMoment.squarefree_divisor_third_moment line 66