OAI/NumberTheory/TwoPoint/Fourier/MinorArcParameterRanges.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Verifying every dyadic hypothesis from the actual prime range.

  1. lemma OAI.TwoPointCorrelations.minor_arc_parameter_range_dyadics line 13
  2. theorem OAI.TwoPointCorrelations.minor_arc_typical_parameter_range_saving line 47