OAI/NumberTheory/DirichletL/Hecke/Signal.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeSignal.quotient line 13
  2. def OAI.SevenEighths.HeckeSignal.amplitude line 16
  3. def OAI.SevenEighths.HeckeSignal.signal line 19
  4. theorem OAI.SevenEighths.HeckeSignal.quotient_differentiableAt line 22
  5. theorem OAI.SevenEighths.HeckeSignal.quotient_bound line 29
  6. theorem OAI.SevenEighths.HeckeSignal.normalizedSignal_eq line 43
  7. theorem OAI.SevenEighths.HeckeSignal.signal_eq_contour line 53
  8. def OAI.SevenEighths.HeckeSignal.quotientBound line 71
  9. theorem OAI.SevenEighths.HeckeSignal.quotientBound_nonneg line 73
  10. theorem OAI.SevenEighths.HeckeSignal.amplitude_continuous_line line 77
  11. theorem OAI.SevenEighths.HeckeSignal.amplitude_norm_bound line 89
  12. theorem OAI.SevenEighths.HeckeSignal.amplitude_integrable_line line 103
  13. theorem OAI.SevenEighths.HeckeSignal.contour_shift line 111
  14. def OAI.SevenEighths.HeckeSignal.endpointConstant line 136
  15. theorem OAI.SevenEighths.HeckeSignal.endpointConstant_nonneg line 140
  16. theorem OAI.SevenEighths.HeckeSignal.signal_bound_at_zero line 146
  17. theorem OAI.SevenEighths.HeckeSignal.signal_rapidDecayAtZero line 166
  18. theorem OAI.SevenEighths.HeckeSignal.amplitude_integrable_reflected line 181
  19. theorem OAI.SevenEighths.HeckeSignal.amplitude_continuous_reflected line 193
  20. theorem OAI.SevenEighths.HeckeSignal.signal_continuousOn line 204
  21. theorem OAI.SevenEighths.HeckeSignal.signal_locallyIntegrable line 231
  22. theorem OAI.SevenEighths.HeckeSignal.signalMellin_eq_amplitude_on_line line 237