OAI/NumberTheory/TwoPoint/Fourier/MajorArcGlobalMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Global typical means for each character in the exact gcd decomposition. The quotient volume is retained before the divisor sum is taken.

  1. lemma OAI.TwoPointCorrelations.major_arc_character_volume line 13
  2. theorem OAI.TwoPointCorrelations.major_arc_typical_rational_global line 34