OAI/NumberTheory/TwoPoint/Fourier/MinorArcParameterSaving.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The minor-arc fourth-root estimate retains the freely chosen Diophantine parameter. This permits a common parameter in both arcs.

  1. lemma OAI.TwoPointCorrelations.minor_arc_parameter_fourth_root line 12
  2. theorem OAI.TwoPointCorrelations.minor_arc_dyadic_parameter_saving line 45