OAI/NumberTheory/CubicMoment/Estimates/LargeTupleSmoothIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Each actual large-row norm piece is a product of the independently smooth coordinate weights. Its only remaining sharp restriction is the original lower bound for the distinguished product.

  1. lemma OAI.CubicFirstMoment.largeTupleCoordinateWeight_product line 14
  2. lemma OAI.CubicFirstMoment.largePrimeTupleTerm_smoothed line 31
  3. theorem OAI.CubicFirstMoment.largePrimeTuplePiece_eq_smooth line 46