OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every fixed divisor moment on primary squarefree elements follows from the finite Euler product and the already specified ordinary prime theorem.

  1. lemma OAI.CubicFirstMoment.squarefree_fixed_reciprocal_sum line 12
  2. lemma OAI.CubicFirstMoment.squarefree_fixed_sum_le_euler line 35
  3. theorem OAI.CubicFirstMoment.squarefree_fixed_divisor_moment line 66