OAI/NumberTheory/TwoPoint/Halasz/HalaszLongShortCongruences.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The congruence energy bound for the actual long/short monomial system. No abstract analytic input occurs in this finite counting step.

  1. def OAI.TwoPointCorrelations.halaszNatPowerFrequency line 12
  2. def OAI.TwoPointCorrelations.halaszLongShortFrequency line 15
  3. def OAI.TwoPointCorrelations.halaszLongResidues line 20
  4. lemma OAI.TwoPointCorrelations.halasz_long_short_congruence line 24
  5. theorem OAI.TwoPointCorrelations.halasz_long_short_congruence_energy line 44