OAI/NumberTheory/Ostmann/ZeroDensity/RealPrimeSeries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The real prime series for a real Dirichlet character

  1. def OAI.Ostmann.realPrimeTerm line 12
  2. theorem OAI.Ostmann.primeLogTerm_ofReal line 15
  3. theorem OAI.Ostmann.exists_realPrimeSeries_error line 32

    Source documentation

    The uniform prime-power error is retained for the actual real weighted prime sum. This result requires no analytic input beyond proved Mathlib.

    theorem exists_realPrimeSeries_error :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℝ q) (s : ℝ), 1 < s →
      Summable (realPrimeTerm χ s) ∧
      |(∑' n, realPrimeTerm χ s n) +
        (deriv (DirichletCharacter.LFunction (χ.ringHomComp Complex.ofRealHom)) (s : ℂ) /
          DirichletCharacter.LFunction (χ.ringHomComp Complex.ofRealHom) (s : ℂ)).re| ≤ C := by
…

    Mentions: OAI.Ostmann.realPrimeTerm