OAI/NumberTheory/TwoPoint/Halasz/HalaszShiftedLongShort.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A common short-variable residue is represented as p*u-a with 0<=a<p. Translating the whole system by a leaves positive long variables and short variables divisible by p.

  1. def OAI.TwoPointCorrelations.halaszShiftedLongShortFrequency line 14
  2. def OAI.TwoPointCorrelations.halaszCommonResidueFrequency line 19
  3. lemma OAI.TwoPointCorrelations.halasz_common_residue_translate line 24
  4. lemma OAI.TwoPointCorrelations.halasz_shifted_long_short_congruence line 49
  5. theorem OAI.TwoPointCorrelations.halasz_shifted_long_short_congruence_energy line 67
  6. lemma OAI.TwoPointCorrelations.halasz_shifted_long_short_refined_energy line 88
  7. theorem OAI.TwoPointCorrelations.halasz_common_residue_energy line 124