OAI/NumberTheory/Ostmann/ZeroDensity/SiegelBoundProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Siegel's bound for the actual primitive real zeros

The proved quadratic L-value estimate is combined with a small-power bound for the derivative in a fixed strip. Constants may depend on the exponent.

  1. theorem OAI.Ostmann.publishedSiegelBound line 15