OAI/NumberTheory/TwoPoint/Halasz/HalaszScaleFactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalizing the long/short scale in the classical recurrence. The loss is a fixed exponential in the moment order.

  1. lemma OAI.TwoPointCorrelations.halasz_scale_factor line 9
  2. lemma OAI.TwoPointCorrelations.halasz_classical_defect_step line 42