OAI/NumberTheory/TwoPoint/Fourier/MinorArcTheorem.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The minor-arc part of corrected MRT, Section 3: the literal typical-set short integral has the required log-log over log saving.

  1. theorem OAI.TwoPointCorrelations.minor_arc_typical_short_bound line 12