OAI/NumberTheory/CubicMoment/Estimates/RoughRemainderArity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual rough remainder is a finite sum of independent prime convolutions. The factorial weight, literal product and roughness cutoff are retained. This is the second arity expansion needed for the large rows.

  1. def OAI.CubicFirstMoment.roughTupleCoefficient line 15
  2. lemma OAI.CubicFirstMoment.roughProduct_as_tuple line 20
  3. lemma OAI.CubicFirstMoment.roughTupleCoefficient_zero_of_card_ne line 28
  4. lemma OAI.CubicFirstMoment.roughProduct_eq_sum_tuples line 42
  5. theorem OAI.CubicFirstMoment.eventually_rough_coefficient_tuples line 67