OAI/NumberTheory/TwoPoint/Halasz/HalaszShortL1.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The typical-set error is linear in its density in the published L1 norm. No square root of the discarded density is introduced.

  1. lemma OAI.TwoPointCorrelations.halasz_short_integral_cells line 14
  2. lemma OAI.TwoPointCorrelations.halasz_window_shift line 32
  3. lemma OAI.TwoPointCorrelations.halasz_translated_bad_count line 36
  4. theorem OAI.TwoPointCorrelations.halasz_typical_short_L1 line 57