OAI/NumberTheory/Ostmann/Characters/CharacterHorizontalGrowth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial logarithmic-derivative bounds along both horizontal edges

  1. theorem OAI.Ostmann.exists_character_horizontal_bound line 13

    Source documentation

    One height controls both horizontal edges of the actual rectangular contour.

    theorem exists_character_horizontal_bound (χ : PrimitiveComplexCharacter) :
    ∃ K : ℝ, 0 < K ∧ ∀ T : ℝ, 3 ≤ T → ∃ t : ℝ,
      T < t ∧ t < T + 1 ∧ (∀ z ∈ complexCharacterZeros χ, |z.im| ≠ t) ∧
      ∀ y : ℝ, y = t ∨ y = -t → ∀ σ ∈ Icc (-(1 / 2 : ℝ)) 2,
        ‖logDeriv χ.L ((σ : ℂ) + (y : ℂ) * I)‖ ≤ K * (T + 5) ^ 3 := by
…

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