CharacterRightZeroCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative zero count in the right half of the critical strip

theorem OAI.Ostmann.PrimitiveComplexCharacter.right_zero_sum_bound line 13

Source documentation

Sum of actual analytic multiplicities over any finite right-half family.

theorem PrimitiveComplexCharacter.right_zero_sum_bound (χ : PrimitiveComplexCharacter)
    (T : ℝ) (hT : 0 ≤ T) (S : Finset ℂ)
    (hS : ∀ z ∈ S, 1 / 2 ≤ z.re ∧ z.re ≤ 1 ∧ |z.im| ≤ T) :
    ∑ z ∈ S, (characterZeroOrder χ z : ℝ) ≤
      (2 * T + 2) * (Real.log (48 * (χ.modulus : ℝ) * (T + 3)) / Real.log (14 / 13)) := by
…

Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.characterZeroOrder