OAI/NumberTheory/Ostmann/ZeroDensity/ActualPageUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Page uniqueness for the actual primitive real zeros

The one-pole bound for two distinct characters and positivity of the actual zero sums give an absolute Landau–Page constant. No uniqueness input is used.

  1. theorem OAI.Ostmann.exists_actual_page_uniqueness line 16