OAI/NumberTheory/Ostmann/Characters/CharacterUnitParseval.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parseval on the full group of Dirichlet characters

The complete unit-group orthogonality is needed before restricting to primitive characters; applying Cauchy--Schwarz separately would lose the conductor.

  1. theorem OAI.Ostmann.character_unit_gram line 16
  2. theorem OAI.Ostmann.character_unit_parseval line 33