OAI/NumberTheory/TwoPoint/Fourier/MajorArcDivisors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Resolving a rational phase on each gcd stratum. The coefficients are finite unit-group Fourier coefficients, so their total mass is controlled by the square root of the reduced modulus.

  1. lemma OAI.TwoPointCorrelations.major_arc_rational_val line 16
  2. lemma OAI.TwoPointCorrelations.major_arc_character_inversion_nat line 21
  3. lemma OAI.TwoPointCorrelations.major_arc_divisor_quotient_pos line 29
  4. def OAI.TwoPointCorrelations.majorArcDivisorTerm line 34
  5. lemma OAI.TwoPointCorrelations.major_arc_divisor_term line 42
  6. theorem OAI.TwoPointCorrelations.major_arc_divisor_expansion line 85