OAI/NumberTheory/TwoPoint/Fourier/MajorArcGCD.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Gcd strata of a rational additive phase. The unit character expansion on the quotient is supported on exactly one divisor of the modulus.

  1. lemma OAI.TwoPointCorrelations.major_arc_reduced_unit_iff line 13
  2. lemma OAI.TwoPointCorrelations.major_arc_gcd_phase line 30
  3. lemma OAI.TwoPointCorrelations.major_arc_gcd_partition line 47

    Source documentation

    The reduced unit projector partitions every positive argument, including arguments in nonunit residue classes and reduced modulus one.

    lemma major_arc_gcd_partition (q n : ℕ) (hq : 0 < q) (_hn : 0 < n)
    (r : ℤ) :
    (∑ d ∈ q.divisors, if d∣n then
      if IsUnit ((n/d:ℕ):ZMod (q/d)) then
        additiveCharacter ((r:ℝ)/((q/d:ℕ):ℝ)) (n/d) else 0 else 0) =
      additiveCharacter ((r:ℝ)/q) n := by
…

    Mentions: OAI.TwoPointCorrelations.additiveCharacter