OAI/NumberTheory/TwoPoint/Fourier/MinorArcWorkingBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The typical minor-arc estimate at the common working length. Both the fourth-root saving and the prime-square remainder fit one rate.

  1. theorem OAI.TwoPointCorrelations.minor_arc_typical_working_bound line 12