OAI/NumberTheory/Ostmann/ZeroDensity/ActualLocalZeros.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Canonical local exceptional zeros

An actual near-one zero is selected when one exists. Its uniqueness and completeness follow from the proved Page theorem, not an analytic input.

  1. def OAI.Ostmann.actualPageConstant line 13
  2. theorem OAI.Ostmann.actualPageConstant_pos line 15
  3. theorem OAI.Ostmann.actualPage_unique line 18
  4. def OAI.Ostmann.actualLocalZero line 24
  5. theorem OAI.Ostmann.actualLocalZero_spec line 30
  6. theorem OAI.Ostmann.actualLocalZero_complete line 42