OAI/NumberTheory/Ostmann/Characters/MellinDiagonal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Mellin Parseval on a multiplicative diagonal

This is the finite interchange of Mellin expansion and a weighted sum used at the beginning of the proof of the uniform estimate src42.

  1. theorem OAI.Ostmann.mellinCoefficient_of_expansion line 19
  2. def OAI.Ostmann.mellinDiagonal line 43
  3. def OAI.Ostmann.mellinDiagonalCoefficient line 48
  4. theorem OAI.Ostmann.mellinDiagonal_expansion line 53
  5. theorem OAI.Ostmann.mellinDiagonal_coefficient line 71
  6. theorem OAI.Ostmann.mellinDiagonal_parseval line 77