OAI/NumberTheory/CubicMoment/Estimates/PrimeTupleCenteredCollection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact collection against the centered kernel. Its vanishing on nonsquarefree products justifies the separate squarefree convolutions; mutual coprimality remains in the original centered kernel.

  1. lemma OAI.CubicFirstMoment.centered_ordered_to_squarefree line 16
  2. lemma OAI.CubicFirstMoment.full_prime_centered_collection line 46
  3. lemma OAI.CubicFirstMoment.full_prime_squarefree_centered_collection line 70