CharacterLocalZeroCount.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local zero counts for primitive character L-functions

Jensen's formula is applied to disks centered on Re(s)=2. The larger radius stays in the positive half-plane; the smaller disk covers a unit ordinate interval in the right half of the critical strip.

def OAI.Ostmann.characterZeroCenter line 18
theorem OAI.Ostmann.characterZeroCenter_re line 20
theorem OAI.Ostmann.characterZeroCenter_im line 23
theorem OAI.Ostmann.characterZeroCenter_norm line 26
theorem OAI.Ostmann.character_disk_re line 29
theorem OAI.Ostmann.character_disk_norm line 36
theorem OAI.Ostmann.PrimitiveComplexCharacter.L_disk_bound line 43
def OAI.Ostmann.characterLocalZeroMass line 58
theorem OAI.Ostmann.PrimitiveComplexCharacter.local_zero_mass_bound line 62
Source documentation
A logarithmic zero count, including analytic multiplicity, on each local disk.
```
theorem PrimitiveComplexCharacter.local_zero_mass_bound (χ : PrimitiveComplexCharacter)
    (t : ℝ) :
    (characterLocalZeroMass χ t : ℝ) ≤
      Real.log (48 * (χ.modulus : ℝ) * (|t| + 2)) / Real.log (14 / 13) := by
…
```
Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterLocalZeroMass