OAI/NumberTheory/DirichletL/Hecke/SignalShift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeSignalShift.quotient_holomorphic line 12
2. theorem OAI.SevenEighths.HeckeSignalShift.quotient_polynomial_bound line 21
3. theorem OAI.SevenEighths.HeckeSignalShift.contour_shift_left line 39
4. def OAI.SevenEighths.HeckeSignalShift.infinityConstant line 72
5. theorem OAI.SevenEighths.HeckeSignalShift.signal_bound_at_infinity line 76
6. theorem OAI.SevenEighths.HeckeSignalShift.signal_isBigO_atTop line 104