OAI/NumberTheory/Ostmann/ZeroDensity/CharacterZeroMultiplicity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual analytic multiplicities of character zeros

The divisor on the whole plane is used consistently, so local disk counts and later sums over finitely many zeros count the same multiplicities.

  1. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_analytic line 16
  2. theorem OAI.Ostmann.PrimitiveComplexCharacter.L_order_ne_top line 21
  3. def OAI.Ostmann.characterZeroOrder line 29
  4. theorem OAI.Ostmann.characterZeroOrder_nonneg line 32
  5. theorem OAI.Ostmann.characterZeroOrder_eq_local line 36
  6. theorem OAI.Ostmann.characterZeroOrder_sum_le_local line 46