OAI/NumberTheory/TwoPoint/Fourier/MajorArcCharacters.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative Fourier resolution of the reduced, unit progression in MRT section 4. The original residue need not be a unit: this lemma is applied after taking out its common divisor with the modulus.

  1. lemma OAI.TwoPointCorrelations.major_arc_unit_indicator line 16
  2. lemma OAI.TwoPointCorrelations.major_arc_unit_progression line 27
  3. lemma OAI.TwoPointCorrelations.major_arc_unit_progression_norm line 50
  4. lemma OAI.TwoPointCorrelations.major_arc_typical_twist line 64