OAI/NumberTheory/TwoPoint/Fourier/MinorArcCofactorCutoff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite cofactor cutoff needed by the literal short-window sum.

  1. lemma OAI.TwoPointCorrelations.minor_arc_cofactor_cutoff line 12
  2. lemma OAI.TwoPointCorrelations.minor_arc_cofactor_cutoff_bound line 19
  3. lemma OAI.TwoPointCorrelations.minor_arc_origin_factor_bound line 35
  4. lemma OAI.TwoPointCorrelations.minor_arc_cofactor_total_bound line 45