OAI/NumberTheory/TwoPoint/Halasz/HalaszShortMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Convert the actual typical short-sum energy to the published L1 quantity while retaining the linear error from discarded integers.

  1. lemma OAI.TwoPointCorrelations.halasz_short_square_cells line 13
  2. lemma OAI.TwoPointCorrelations.halasz_short_mean_square line 46
  3. theorem OAI.TwoPointCorrelations.halasz_short_mean_transfer line 64