OAI/NumberTheory/JointDickman/Probability/KernelDenominatorSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A sufficient subpower bound for the kernel denominator sum

Mertens' product theorem and the harmonic sum bound suffice here. A polylogarithmic bound is enough to absorb either of the manuscript's positive power savings, so no additional mean-value theorem is assumed.

  1. def OAI.JointDickman.kernelDenominatorSum line 17
  2. theorem OAI.JointDickman.kernelDenominatorSum_log_bound line 20
  3. theorem OAI.JointDickman.kernelDenominatorSum_subpower line 59