OAI/NumberTheory/TwoPoint/Fourier/MinorArcWorkingParameters.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal first band satisfies all minor-arc support conditions once the common parameter exceeds a fixed threshold.

  1. theorem OAI.TwoPointCorrelations.minor_arc_actual_working_parameters line 13