OAI/NumberTheory/Ostmann/ZeroDensity/CharacterSiegelTools.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bridges from the proved Siegel value bound to actual real zeros

The three reused character-analysis modules are the unchanged completed result 028 sources at f5371230bbb5024338caeeb3a6eaf46fb2cd4842. The derivative bridge below specializes their regular Dirichlet-series bound near the line Re(s)=1.

  1. theorem OAI.Ostmann.real_character_quadratic line 17
  2. theorem OAI.Ostmann.character_deriv_small_power line 29
  3. theorem OAI.Ostmann.character_zero_value_bound line 49