OAI/NumberTheory/Ostmann/ZeroDensity/NonprincipalLogDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic-derivative lower bound at an arbitrary character level

  1. def OAI.Ostmann.primitiveOfNonprincipal line 12
  2. theorem OAI.Ostmann.primitiveOfNonprincipal_logDeriv_difference line 23
  3. theorem OAI.Ostmann.exists_nonprincipal_logDeriv_real_lower line 33

    Source documentation

    Only a logarithmic modulus loss is incurred by imprimitive characters.

    theorem exists_nonprincipal_logDeriv_real_lower : ∃ B : ℝ, 0 < B ∧
    ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q), χ ≠ 1 →
      ∀ s : ℂ, 1 < s.re → s.re ≤ 2 →
        -(3 / 2) * Real.log q - B * Real.log (|s.im| + 2) ≤
          (logDeriv (DirichletCharacter.LFunction χ) s).re := by
…