OAI/NumberTheory/TwoPoint/Fourier/MinorArcPrimeKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The four-prime kernel in MRT (3.3), including arbitrary window lengths.

  1. theorem OAI.TwoPointCorrelations.minor_arc_prime_difference_kernel line 13
  2. theorem OAI.TwoPointCorrelations.minor_arc_prime_kernel_rational line 57