theorem DirichletCharacter.twistedSmoothedPerronIntegrand_integrable_right {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) : MeasureTheory.Integrable (fun (t : ℝ) => χ.twistedSmoothedPerronIntegrand ν ε X (↑σ + ↑t * Complex.I)) MeasureTheory.volume

On every standard right Perron line, the twisted smoothed Perron integrand is integrable. The proof uses the absolutely convergent von Mangoldt Dirichlet-series majorant and the integrability of the Mellin smoothing factor.

theorem DirichletCharacter.twistedSmoothedPerron_verticalIntegral_split_three {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) (T : ℝ) : VerticalIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) σ = (Complex.I • ∫ (t : ℝ) in Set.Iic (-T), χ.twistedSmoothedPerronIntegrand ν ε X (↑σ + ↑t * Complex.I)) + VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) σ (-T) T + Complex.I • ∫ (t : ℝ) in Set.Ici T, χ.twistedSmoothedPerronIntegrand ν ε X (↑σ + ↑t * Complex.I)

The right vertical integral is the sum of its lower tail, the finite vertical segment from -T to T, and its upper tail.