OAI/NumberTheory/DirichletL/TraceCharacter.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.TraceCharacter.O line 12
  2. def OAI.SevenEighths.TraceCharacter.traceCharacter line 17
  3. theorem OAI.SevenEighths.TraceCharacter.traceCharacter_mk line 21
  4. theorem OAI.SevenEighths.TraceCharacter.traceCharacter_eq_paperE line 26
  5. theorem OAI.SevenEighths.TraceCharacter.traceCharacter_isPrimitive line 31
  6. theorem OAI.SevenEighths.TraceCharacter.residue_card line 40
  7. def OAI.SevenEighths.TraceCharacter.gaussScalar line 44
  8. theorem OAI.SevenEighths.TraceCharacter.transform_nonunit line 47
  9. theorem OAI.SevenEighths.TraceCharacter.transform_eq line 52
  10. theorem OAI.SevenEighths.TraceCharacter.paper_transform_eq line 58
  11. theorem OAI.SevenEighths.TraceCharacter.gaussScalar_norm_sq line 67
  12. theorem OAI.SevenEighths.TraceCharacter.gaussScalar_norm line 74
  13. theorem OAI.SevenEighths.TraceCharacter.gaussScalar_norm_embedding line 79
  14. theorem OAI.SevenEighths.TraceCharacter.gaussScalar_ne_zero line 85
  15. def OAI.SevenEighths.TraceCharacter.normalizedGauss line 90
  16. theorem OAI.SevenEighths.TraceCharacter.normalizedGauss_norm line 93
  17. theorem OAI.SevenEighths.TraceCharacter.character_expansion line 99
  18. theorem OAI.SevenEighths.TraceCharacter.primitive_paper_poisson line 106
  19. theorem OAI.SevenEighths.TraceCharacter.primitive_radial_paper_poisson line 126
  20. theorem OAI.SevenEighths.TraceCharacter.primitive_radial_paper_poisson_normalized line 149