noncomputable def DirichletCharacter.twistedVonMangoldtCoeff {q : ℕ} (χ : DirichletCharacter ℂ q) (n : ℕ) : ℂ

The coefficients of the negative logarithmic derivative of a Dirichlet L-function, in the order used by the smoothed prime sum.

Equations

• χ.twistedVonMangoldtCoeff n = ↑(ArithmeticFunction.vonMangoldt n) * χ ↑n

noncomputable def DirichletCharacter.twistedSmoothedPsi {q : ℕ} (χ : DirichletCharacter ℂ q) (ν : ℝ → ℝ) (ε X : ℝ) : ℂ

The genuinely infinite smoothed twisted Chebyshev sum.

Equations

• χ.twistedSmoothedPsi ν ε X = ∑' (n : ℕ), χ.twistedVonMangoldtCoeff n * ↑(Smooth1 ν ε (↑n / X))

noncomputable def DirichletCharacter.twistedSmoothedPerronIntegrand {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (ν : ℝ → ℝ) (ε X : ℝ) (s : ℂ) : ℂ

The integrand in the twisted smoothed Perron formula.

Equations

• χ.twistedSmoothedPerronIntegrand ν ε X s = -deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s * mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) s * ↑X ^ s

theorem DirichletCharacter.neg_logDeriv_LFunction_eq_tsum_twistedVonMangoldtCoeff {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : -deriv (LFunction χ) s / LFunction χ s = ∑' (n : ℕ), χ.twistedVonMangoldtCoeff n / ↑n ^ s

theorem DirichletCharacter.twistedSmoothedPerron_aux_tsum_integral {q : ℕ} (χ : DirichletCharacter ℂ q) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {X : ℝ} (X_pos : 0 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) {σ : ℝ} (σ_gt : 1 < σ) (σ_le : σ ≤ 2) : ∫ (t : ℝ), ∑' (n : ℕ), χ.twistedVonMangoldtCoeff n / ↑n ^ (↑σ + ↑t * Complex.I) * mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) (↑σ + ↑t * Complex.I) * ↑X ^ (↑σ + ↑t * Complex.I) = ∑' (n : ℕ), ∫ (t : ℝ), χ.twistedVonMangoldtCoeff n / ↑n ^ (↑σ + ↑t * Complex.I) * mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) (↑σ + ↑t * Complex.I) * ↑X ^ (↑σ + ↑t * Complex.I)

theorem DirichletCharacter.twistedSmoothedPerron {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {X : ℝ} (X_pos : 0 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) {σ : ℝ} (σ_gt : 1 < σ) (σ_le : σ ≤ 2) : χ.twistedSmoothedPsi ν ε X = VerticalIntegral' (χ.twistedSmoothedPerronIntegrand ν ε X) σ

Smoothed Perron inversion for the von Mangoldt coefficients twisted by an arbitrary Dirichlet character. No nonprincipality assumption and no contour shift are used.