OAI/NumberTheory/CubicMoment/Estimates/SmallTwistSmoothMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original primary mixed smooth sum has the cubic second moment. Its primitive characters, conductors, and Euler corrections are constructed.

  1. def OAI.CubicFirstMoment.primarySmallTwistSmoothSum line 16
  2. theorem OAI.CubicFirstMoment.primary_smalltwist_smooth_cubic_moment line 20