OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterFourier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite multiplicative Fourier inversion on the unit residues. The L1 coefficient bound follows from Parseval and Cauchy--Schwarz and requires no primitive-character or Gauss-sum estimate.

  1. def OAI.TwoPointCorrelations.mrtCharacterFourierCoefficient line 16
  2. lemma OAI.TwoPointCorrelations.mrt_character_fourier_kernel line 20
  3. theorem OAI.TwoPointCorrelations.mrt_character_fourier_inversion line 37
  4. lemma OAI.TwoPointCorrelations.mrt_character_coefficient_conj line 68
  5. theorem OAI.TwoPointCorrelations.mrt_character_fourier_parseval line 75
  6. theorem OAI.TwoPointCorrelations.mrt_character_fourier_l1 line 116
  7. def OAI.TwoPointCorrelations.mrtAdditiveCharacterCoefficient line 143
  8. theorem OAI.TwoPointCorrelations.mrt_additive_character_inversion line 147
  9. theorem OAI.TwoPointCorrelations.mrt_additive_character_l1 line 152