OAI/NumberTheory/TwoPoint/Halasz/HalaszDyadicCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A dyadic cutoff comparable with the square of the height, with the precise height-to-length margin needed by the phase estimate.

  1. def OAI.TwoPointCorrelations.halaszDyadicCutoffDegree line 9
  2. lemma OAI.TwoPointCorrelations.halasz_dyadic_cutoff_bounds line 11