OAI/NumberTheory/CubicMoment/Estimates/PrimeTupleRegrouping.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact regrouping of independently weighted prime coordinates into two product variables. The grouping is fixed for the whole box.

  1. lemma OAI.CubicFirstMoment.independent_tuple_sum_split line 14
  2. lemma OAI.CubicFirstMoment.independent_prime_tuple_bilinear line 36