Theorem: MellinInversion_aux2 (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
s : ℂ
fDiff : DifferentiableOn ℝ f (Ioi 0)
fDiff2 : DifferentiableOn ℝ (deriv f) (Ioi 0)
hfs : Tendsto (fun x => deriv f x * ↑x ^ s) (𝓝[>] 0) (𝓝 0)
hfinf : Tendsto (fun x => deriv f x * ↑x ^ s) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, deriv f x * ↑x ^ s = -∫ (x : ℝ) in Ioi 0, deriv (deriv f) x * ↑x ^ (s + 1) / (s + 1)
Tactic:
sorry
State after:
no goals