OAI/NumberTheory/TwoPoint/Halasz/HalaszCubicLaplace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cubic Laplace estimate used to pass from the logarithmic exponential-sum bound to the Vinogradov--Korobov zeta bound (Ford, Proc. LMS 85 (2002), Section 7). Absolute constants are deliberately weakened; only the exponents 3/2 and 2/3 matter for the application.

  1. lemma OAI.TwoPointCorrelations.halasz_cubic_balance line 15
  2. lemma OAI.TwoPointCorrelations.halasz_cubic_kernel_integrable line 47
  3. lemma OAI.TwoPointCorrelations.halasz_cubic_kernel_integral line 56
  4. theorem OAI.TwoPointCorrelations.halasz_cubic_laplace_bound line 77