OAI/NumberTheory/Ostmann/Dirichlet/WideNormalizedDisk.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Dirichlet.wideDirichletDiskPoint line 13
  2. def OAI.Ostmann.Dirichlet.wideNormalizedDirichlet line 14
  3. def OAI.Ostmann.Dirichlet.wideDirichletDiskEnvelope line 18
  4. theorem OAI.Ostmann.Dirichlet.wideDirichletDiskPoint_re line 21
  5. theorem OAI.Ostmann.Dirichlet.wideDirichletDiskPoint_half_strip line 25
  6. theorem OAI.Ostmann.Dirichlet.wideDirichletDiskPoint_norm line 31
  7. theorem OAI.Ostmann.Dirichlet.wideNormalizedDirichlet_zero line 42
  8. theorem OAI.Ostmann.Dirichlet.wideNormalizedDirichlet_analytic line 48
  9. theorem OAI.Ostmann.Dirichlet.wideNormalizedDirichlet_bound line 57
  10. theorem OAI.Ostmann.Dirichlet.wideDirichletDiskEnvelope_gt_one line 82