OAI/NumberTheory/TwoPoint/Halasz/HalaszHurwitzCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

First-order Euler truncation for the actual Hurwitz function, uniform in the shift after its first term is removed.

  1. lemma OAI.TwoPointCorrelations.halasz_zeta_cutoff line 12
  2. theorem OAI.TwoPointCorrelations.halasz_hurwitz_cutoff line 51