OAI/NumberTheory/Jacobsthal/Primes/DirichletZeroPenalty.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletCenter line 12
  2. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskPoint line 13
  3. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet line 14
  4. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskEnvelope line 18
  5. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletCenter_re line 21
  6. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskPoint_re line 23
  7. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskPoint_half_strip line 27
  8. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskPoint_norm line 33
  9. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet_zero line 44
  10. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet_analytic line 50
  11. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet_bound line 59
  12. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskEnvelope_gt_one line 75
  13. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet_zero_re_lt line 86
  14. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.log_dirichletDiskEnvelope_bound line 105
  15. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet_log_derivative line 126
  16. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.uniform_dirichlet_local_log_derivative line 144
  17. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.dirichletDiskPoint_ofReal line 192
  18. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.real_zero_term_nonneg line 198
  19. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.uniform_neg_real_log_derivative line 205
  20. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.normalizedDirichlet_zero_order_pos line 256
  21. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.uniform_zero_penalty line 271