OAI/NumberTheory/TwoPoint/Halasz/HalaszDyadicScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The dyadic blocks above the square-root cutoff stay inside the original pretentious scale, with uniform logarithmic errors.

  1. lemma OAI.TwoPointCorrelations.halasz_dyadic_original_scale line 10
  2. lemma OAI.TwoPointCorrelations.halasz_dyadic_error_comparison line 25
  3. lemma OAI.TwoPointCorrelations.halasz_dyadic_short_height line 38
  4. lemma OAI.TwoPointCorrelations.halasz_log_le_two_sqrt line 43
  5. lemma OAI.TwoPointCorrelations.halasz_sqrt_cutoff_error line 49