exact contourPull (by linarith) (not_mem_uIcc_of_gt (by linarith) (by linarith))
  (not_mem_uIcc_of_gt (by linarith) (by linarith))
case e_a
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x_gt_one : 1 < x
σ'le : σ' ≤ -3 / 2
σ''le : σ'' ≤ -3 / 2
⊢ VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ' = VerticalIntegral (fun s => ↑x ^ s / (s * (s + 1))) σ''
no goals