OAI/NumberTheory/Ostmann/ZeroDensity/ComplexCharacterTrigonometric.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The 3-4-1 Euler inequality for every complex Dirichlet character

  1. theorem OAI.Ostmann.complex_character_polynomial_nonneg line 12
  2. theorem OAI.Ostmann.complex_character_trigonometric_term_nonneg line 20
  3. theorem OAI.Ostmann.dirichlet_mangoldt_LSeries_eq line 50
  4. theorem OAI.Ostmann.complex_character_trigonometric_sum_nonneg line 58