OAI/NumberTheory/Ostmann/ZeroDensity/PrimeLogDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The prime logarithmic series and the actual L-function derivative

  1. def OAI.Ostmann.primeLogCoefficients line 13
  2. theorem OAI.Ostmann.twisted_vonMangoldt_decomposition line 16
  3. theorem OAI.Ostmann.exists_primeLogDerivative_error line 26

    Source documentation

    Removing prime powers from the proved Euler identity costs only an absolute bounded error, uniformly in the character and s > 1.

    theorem exists_primeLogDerivative_error :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℝ), 1 < s →
      LSeriesSummable (primeLogCoefficients χ) (s : ℂ) ∧
      ‖LSeries (primeLogCoefficients χ) (s : ℂ) +
        deriv (DirichletCharacter.LFunction χ) (s : ℂ) /
          DirichletCharacter.LFunction χ (s : ℂ)‖ ≤ C := by
…

    Mentions: OAI.Ostmann.primeLogCoefficients