LowHeightZeroBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.shifted_real_zero_sum_nonneg line 14
theorem OAI.Ostmann.shifted_real_zero_term_le line 21
theorem OAI.Ostmann.shifted_real_zero_pair_le line 28
theorem OAI.Ostmann.exists_low_height_zero_sum_error line 39
Source documentation
Uniform upper error after replacing the completed logarithmic derivative by the ordinary one in the actual shifted zero identity.
```
theorem exists_low_height_zero_sum_error : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : PrimitiveRealCharacter) (s : ℂ), 1 < s.re → s.re ≤ 2 → |s.im| ≤ 2 →
      shiftedRealCharacterZeroSum χ s ≤ (logDeriv χ.L s).re +
        (1 / 2) * Real.log χ.modulus + C := by
…
```
Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.shiftedRealCharacterZeroSum
theorem OAI.Ostmann.exists_real_zero_sum_upper line 54
Source documentation
On the real axis the elementary Euler bound gives a single pole, uniformly in the primitive real character.
```
theorem exists_real_zero_sum_upper : ∃ C : ℝ, 0 < C ∧
    ∀ (χ : PrimitiveRealCharacter) (s : ℝ), 1 < s → s ≤ 2 →
      shiftedRealCharacterZeroSum χ (s : ℂ) ≤ 1 / (s - 1) +
        (1 / 2) * Real.log χ.modulus + C := by
…
```
Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.shiftedRealCharacterZeroSum
theorem OAI.Ostmann.exists_low_height_vonMangoldt_upper line 69