have tpos : 0 < t := by linarith
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t