OAI/NumberTheory/TwoPoint/Halasz/HalaszHurwitzGrowth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial logarithmic growth of the actual Hurwitz function in a weak Vinogradov--Korobov strip, uniform in the translation parameter.

  1. theorem OAI.TwoPointCorrelations.halasz_hurwitz_growth line 13