OAI/NumberTheory/TwoPoint/Halasz/HalaszLogDirichletBlock.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform Dirichlet block bounds in the weak Vinogradov--Korobov strip. The harmless power of the height replaces all degree-selection constants.

  1. theorem OAI.TwoPointCorrelations.halasz_log_dirichlet_block line 13