OAI/NumberTheory/Ostmann/ZeroDensity/LowHeightShiftedBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_low_height_shifted_bound line 13

   Source documentation

   The coefficient three on the real pole, and the separate doubled-height pole, give the strict inequality needed to exclude a nonreal exceptional zero.

   theorem exists_low_height_shifted_bound : ∃ C : ℝ, 0 < C ∧
       ∀ (χ : PrimitiveRealCharacter) (σ t : ℝ), 1 < σ → σ ≤ 2 → |t| ≤ 1 →
         4 * shiftedRealCharacterZeroSum χ ((σ : ℂ) + (t : ℂ) * I) ≤
           3 / (σ - 1) + realZeroKernel (σ - 1) (2 * t) +
             2 * Real.log χ.modulus + C := by
   …

   Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.shiftedRealCharacterZeroSum, OAI.Ostmann.realZeroKernel