OAI/NumberTheory/CubicMoment/Estimates/TwistedMomentLoss.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absorption of the exact small-prime partition and dyadic losses.

  1. lemma OAI.CubicFirstMoment.dyad_card_sq_power line 11
  2. theorem OAI.CubicFirstMoment.twisted_moment_loss line 29
  3. theorem OAI.CubicFirstMoment.twisted_moment_weighted_loss line 63