OAI/NumberTheory/CubicMoment/Estimates/LargeTupleKernelIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual regrouped kernel on the full Mellin line. No product cutoff or Mellin-frequency remainder is discarded by these identities.

  1. abbrev OAI.CubicFirstMoment.largeTupleSelectedSupport line 14
  2. abbrev OAI.CubicFirstMoment.largeTupleOtherSupport line 20
  3. abbrev OAI.CubicFirstMoment.largeTupleSelectedCoefficient line 26
  4. abbrev OAI.CubicFirstMoment.largeTupleOtherCoefficient line 32
  5. def OAI.CubicFirstMoment.largeTupleSmoothedPolynomial line 38
  6. theorem OAI.CubicFirstMoment.largeTupleRegroupedKernel_low_integral line 44
  7. theorem OAI.CubicFirstMoment.largeTupleSmoothedPolynomial_mellin line 56