OAI/NumberTheory/TwoPoint/Halasz/HalaszPhaseTranslation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Frequency translation and the actual typical-set coefficient.

  1. lemma OAI.TwoPointCorrelations.halasz_power_phase_frequency_add line 12
  2. lemma OAI.TwoPointCorrelations.halasz_power_phase_twist line 16
  3. lemma OAI.TwoPointCorrelations.halasz_twisted_phase_mean line 25
  4. lemma OAI.TwoPointCorrelations.halasz_twisted_dyadic line 33
  5. lemma OAI.TwoPointCorrelations.halasz_typical_twist line 41