OAI/NumberTheory/TwoPoint/Halasz/HalaszDegreeSelection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative degree choices as a function of log|t|/log N.

  1. lemma OAI.TwoPointCorrelations.halasz_large_degree_selection line 10
  2. lemma OAI.TwoPointCorrelations.halasz_large_root_saving line 19