OAI/NumberTheory/DirichletL/Hecke/PrimeDyadicContour.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckePrimeDyadic.integrand line 11
2. theorem OAI.SevenEighths.HeckePrimeDyadic.series_differentiableAt_nonprincipal line 16
3. theorem OAI.SevenEighths.HeckePrimeDyadic.series_differentiableAt_right line 21
4. theorem OAI.SevenEighths.HeckePrimeDyadic.integrand_differentiableAt line 30
5. theorem OAI.SevenEighths.HeckePrimeDyadic.integrand_norm line 42
6. theorem OAI.SevenEighths.HeckePrimeDyadic.integrand_vertical_integrable line 50
7. theorem OAI.SevenEighths.HeckePrimeDyadic.finite_rectangle line 73
8. theorem OAI.SevenEighths.HeckePrimeDyadic.polynomial_finite_shift line 101