OAI/NumberTheory/CubicMoment/Estimates/BoundedDistinguishedCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual distinguished subset coefficient is the finite sum of its fixed-length prime convolutions. The arity cutoff is proved from the lower bound on every prime carrying a nonzero distinguished weight.

  1. lemma OAI.CubicFirstMoment.distinguishedSubsetWeight_eq_sum_tuples line 15
  2. theorem OAI.CubicFirstMoment.eventually_distinguished_coefficient_tuples line 47