OAI/NumberTheory/CubicMoment/Estimates/MixedSmoothMoment.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.primaryMixedSmoothSum line 15
  2. theorem OAI.CubicFirstMoment.primary_mixed_smooth_cubic_moment line 19