OAI/NumberTheory/DirichletL/TraceConductor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.TraceConductor.O line 12
  2. structure OAI.SevenEighths.TraceConductor.PrimitivePresentation line 17
  3. theorem OAI.SevenEighths.TraceConductor.exists_primitivePresentation line 28
  4. def OAI.SevenEighths.TraceConductor.primitivePresentation line 50
  5. def OAI.SevenEighths.TraceConductor.PrimitivePresentation.conductor line 58
  6. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.conductor_ne_bot line 60
  7. def OAI.SevenEighths.TraceConductor.PrimitivePresentation.gauss line 64
  8. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.gauss_norm line 68
  9. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.gauss_ne_zero line 73
  10. def OAI.SevenEighths.TraceConductor.PrimitivePresentation.fourier line 77
  11. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.fourier_eq line 82
  12. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.fourier_nonunit line 87
  13. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.source_sum_eq_masked line 92
  14. def OAI.SevenEighths.TraceConductor.PrimitivePresentation.normalizedGauss line 101
  15. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.normalizedGauss_norm line 105
  16. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.paper_poisson line 110
  17. theorem OAI.SevenEighths.TraceConductor.PrimitivePresentation.radial_paper_poisson line 118