OAI/NumberTheory/JointDickman/Counting/CoefficientMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

First and second moments of the actual coefficient A₀

These are the estimates in equation (5) of the manuscript. The two specializations of the published Selberg–Delange input suffice here.

  1. theorem OAI.JointDickman.roughSquarefreeWeight_sq line 17
  2. theorem OAI.JointDickman.coefficientScale_eq_roughMeanNormalization line 22
  3. theorem OAI.JointDickman.coefficientScale_sq line 26
  4. theorem OAI.JointDickman.coefficient_second_moment_factor line 42
  5. theorem OAI.JointDickman.coefficient_first_moment line 84
  6. theorem OAI.JointDickman.coefficient_second_moment line 98