OAI/NumberTheory/JointDickman/Arithmetic/SmoothCoefficientMinorArc.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The smooth minor-arc bound for the actual coefficient, equation (36)

  1. def OAI.JointDickman.smoothCoefficientAdditiveSum line 12
  2. theorem OAI.JointDickman.coefficient_partial_sum_from_zero line 15
  3. theorem OAI.JointDickman.smooth_coefficient_minorArc_bound line 27