noncomputable def DirichletCharacter.twistedVonMangoldtRightMajorant {q : ℕ} (χ : DirichletCharacter ℂ q) (δ t : ℝ) : ℝ

The natural absolute Dirichlet-series majorant on the line re s = 1 + δ.

Equations

• χ.twistedVonMangoldtRightMajorant δ t = ∑' (n : ℕ), ‖χ.twistedVonMangoldtCoeff n / ↑n ^ (↑(1 + δ) + ↑t * Complex.I)‖

theorem DirichletCharacter.twistedVonMangoldtRightMajorant_le {q : ℕ} (χ : DirichletCharacter ℂ q) {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1) (t : ℝ) : χ.twistedVonMangoldtRightMajorant δ t ≤ 6 * (1 + δ⁻¹ ^ 2)

A completely explicit character- and height-independent estimate for the absolute von Mangoldt Dirichlet series.

theorem DirichletCharacter.twistedSmoothedPerron_right_tails_quantitative {ν : ℝ → ℝ} (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) : ∃ c > 0, ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {δ ε X T : ℝ}, 0 < δ → δ ≤ 1 → 0 < ε → ε < 1 → 0 < X → 1 ≤ T → ‖∫ (t : ℝ) in Set.Iic (-T), χ.twistedSmoothedPerronIntegrand ν ε X (↑(1 + δ) + ↑t * Complex.I)‖ ≤ c * X ^ (1 + δ) * (1 + δ⁻¹ ^ 2) / (ε * T) ∧ ‖∫ (t : ℝ) in Set.Ici T, χ.twistedSmoothedPerronIntegrand ν ε X (↑(1 + δ) + ↑t * Complex.I)‖ ≤ c * X ^ (1 + δ) * (1 + δ⁻¹ ^ 2) / (ε * T)

Quantitative lower and upper tails on the standard right line σ = 1 + δ. The constant is selected before q, χ, δ, ε, X, T, hence depends only on the smoothing function.