OAI/NumberTheory/Ostmann/Dirichlet/RectangleIntegration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Dirichlet.HIntegral line 11
2. def OAI.Ostmann.Dirichlet.VIntegral line 14
3. def OAI.Ostmann.Dirichlet.RectangleIntegral line 17
4. def OAI.Ostmann.Dirichlet.VerticalIntegral line 21
5. lemma OAI.Ostmann.Dirichlet.verticalIntegral_split_three line 24
6. abbrev OAI.Ostmann.Dirichlet.HolomorphicOn line 34
7. theorem OAI.Ostmann.Dirichlet.HolomorphicOn.vanishesOnRectangle line 37