OAI/NumberTheory/CubicMoment/Estimates/ShortTupleMellin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mellin separation for the actual smooth short-inverse factors. The integrand is a product of the original primary sums, with a common shift.

  1. lemma OAI.CubicFirstMoment.mellinPhase_mul_neg_cpow line 14
  2. lemma OAI.CubicFirstMoment.primaryShortSmoothSum_eq_subtype line 24
  3. def OAI.CubicFirstMoment.primaryShortTupleSum line 46
  4. theorem OAI.CubicFirstMoment.primaryShortTupleSum_mellin line 56