OAI/NumberTheory/TwoPoint/Halasz/HalaszShortBoundedLength.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The bounded short-length cases are absorbed by the positive logarithmic term of the published error.

  1. lemma OAI.TwoPointCorrelations.halasz_loglog_ten_pos line 11
  2. lemma OAI.TwoPointCorrelations.halasz_bounded_length_ratio line 17
  3. lemma OAI.TwoPointCorrelations.halasz_short_bounded_length line 40