OAI/NumberTheory/TwoPoint/Fourier/MinorArcLogSaving.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Taking the fourth root after choosing the published minor-arc parameter W = (log H)^5.

  1. lemma OAI.TwoPointCorrelations.minor_arc_log_fourth_root line 13
  2. theorem OAI.TwoPointCorrelations.minor_arc_dyadic_log_saving line 44