OAI/NumberTheory/CubicMoment/Estimates/SquarefreeDivisorMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.CubicFirstMoment.squarefree_four_reciprocal_sum line 12
  2. lemma OAI.CubicFirstMoment.squarefree_four_sum_le_euler line 35
  3. theorem OAI.CubicFirstMoment.squarefree_divisor_second_moment line 66