OAI/NumberTheory/TwoPoint/Halasz/HalaszDegreeSaving.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Numerical margins for the degree and shift-length choices in the logarithmic exponential-sum application.

  1. lemma OAI.TwoPointCorrelations.halasz_low_height_degree_margin line 9
  2. lemma OAI.TwoPointCorrelations.halasz_medium_degree_margin line 16
  3. lemma OAI.TwoPointCorrelations.halasz_small_degree_margin line 21
  4. lemma OAI.TwoPointCorrelations.halasz_small_degree_saving line 26
  5. lemma OAI.TwoPointCorrelations.halasz_large_degree_margin line 36
  6. lemma OAI.TwoPointCorrelations.halasz_large_degree_saving line 41
  7. lemma OAI.TwoPointCorrelations.halasz_small_taylor_exponent line 49
  8. lemma OAI.TwoPointCorrelations.halasz_large_taylor_exponent line 52