OAI/NumberTheory/CubicMoment/Estimates/LogCoefficientEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit logarithmic, rather than subpower, energy of the actual full prime convolution. This is used in the small-conductor sieve range.

  1. theorem OAI.CubicFirstMoment.logarithmic_full_coefficient_energy line 13