OAI/NumberTheory/CubicMoment/Estimates/FirstWeightedTuple.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full first-configuration moment for the actual smooth weighted short-factor tuple. Mellin separation includes the complementary tails.

  1. lemma OAI.CubicFirstMoment.primaryShortTupleSum_integral line 16
  2. theorem OAI.CubicFirstMoment.first_weighted_tuple_power_saving line 33