have : Continuous (fun (y : ℝ) ↦ f x (σ + y * I)) := by
  refine (isHolomorphicOn xpos).continuousOn.comp_continuous (by continuity) fun x ↦ not_or.mpr ?_
  simp [Complex.ext_iff, σ_ne_zero, σ_ne_neg_one]
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
⊢ Integrable (fun t => f x (↑σ + ↑t * I)) volume