CharacterZeroCountRate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Standard conductor-height form of the right-half zero count

theorem OAI.Ostmann.character_zero_log_cost line 11

theorem OAI.Ostmann.PrimitiveComplexCharacter.right_zero_sum_rate line 28

Source documentation

The uniform ordinary zero-count rate on the right half of the critical strip.

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

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