OAI/NumberTheory/TwoPoint/Halasz/HalaszTypicalGlobal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Sum the literal typical energy over dyadic origins. Keeping the coefficient fixed is essential when it is later resolved into characters.

  1. lemma OAI.TwoPointCorrelations.halasz_short_dyadic_cells line 12
  2. theorem OAI.TwoPointCorrelations.halasz_short_global_energy line 30
  3. lemma OAI.TwoPointCorrelations.halasz_sharp_log_error_comparison line 51
  4. lemma OAI.TwoPointCorrelations.halasz_sharp_root_error_comparison line 76