OAI/NumberTheory/Ostmann/ZeroDensity/SmoothHorizontalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fifth-order decay of the actual horizontal contour integrals

  1. def OAI.Ostmann.smoothHorizontalIntegral line 14
  2. theorem OAI.Ostmann.primeMeanMellin_decay_pow line 20
  3. theorem OAI.Ostmann.exists_smooth_horizontal_bound line 34

    Source documentation

    The local logarithmic derivative is at most cubic, while the fixed test has eighth-order Mellin decay. The resulting horizontal integrals decay to zero.

    theorem exists_smooth_horizontal_bound (χ : PrimitiveComplexCharacter) (X : ℝ) (hX : 2 ≤ X) :
    ∃ D : ℝ, 0 < D ∧ ∀ T : ℝ, 3 ≤ T → ∃ t : ℝ,
      T < t ∧ t < T + 1 ∧ (∀ z ∈ complexCharacterZeros χ, |z.im| ≠ t) ∧
      ∀ y : ℝ, y = t ∨ y = -t →
        ‖smoothHorizontalIntegral χ X y‖ ≤ D / (T + 1) ^ 5 := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.complexCharacterZeros, OAI.Ostmann.smoothHorizontalIntegral