OAI/NumberTheory/TwoPoint/Halasz/HalaszResidueAveraging.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging the short-variable moment over residue classes. This is the p^(2s) step in the fundamental complete-system estimate.

  1. lemma OAI.TwoPointCorrelations.halasz_torus_power_sum_bound line 12
  2. theorem OAI.TwoPointCorrelations.halasz_residue_average_energy line 46