OAI/NumberTheory/JointDickman/Analysis/CharacterFourierExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite Fourier expansion of character-twisted logarithmic sums

  1. def OAI.JointDickman.characterFourierCoefficient line 11
  2. lemma OAI.JointDickman.characterFourierCoefficient_norm_le line 15
  3. lemma OAI.JointDickman.character_fourier_expansion line 32
  4. lemma OAI.JointDickman.stdAddChar_mul_int_as_phase line 43
  5. lemma OAI.JointDickman.differencingPhase_add line 54
  6. lemma OAI.JointDickman.character_log_sum_fourier line 58
  7. lemma OAI.JointDickman.character_log_sum_bound line 72