OAI/NumberTheory/CubicMoment/Estimates/LargeTupleSingleton.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of a singleton coordinate of the actual large tuple with the one-prime coefficient. The other coordinates and the smooth total-product weight are retained.

  1. lemma OAI.CubicFirstMoment.largeTupleSmoothedPolynomial_singleton line 16
  2. lemma OAI.CubicFirstMoment.triple_other_card line 58