OAI/NumberTheory/TwoPoint/Halasz/HalaszEnergyRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing a bad collection of tuples costs at most twice its cross-count with all tuples. This keeps both sides of the system good.

  1. lemma OAI.TwoPointCorrelations.halasz_cross_count_self line 12
  2. lemma OAI.TwoPointCorrelations.halasz_cross_count_symm line 21
  3. lemma OAI.TwoPointCorrelations.halasz_cross_count_mono line 33
  4. theorem OAI.TwoPointCorrelations.halasz_energy_restriction line 40