Theorem: PartialIntegration (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
fDiff : DifferentiableOn ℝ f (Ioi 0)
gDiff : DifferentiableOn ℝ g (Ioi 0)
fDerivgInt : IntegrableOn (f * deriv g) (Ioi 0) volume
gDerivfInt : IntegrableOn (deriv f * g) (Ioi 0) volume
lim_at_zero : Tendsto (f * g) (𝓝[>] 0) (𝓝 0)
lim_at_inf : Tendsto (f * g) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv f x * g x
Tactic:
simpa using integral_Ioi_mul_deriv_eq_deriv_mul
  (fun x hx ↦ fDiff.hasDerivAt (Ioi_mem_nhds hx))
  (fun x hx ↦ gDiff.hasDerivAt (Ioi_mem_nhds hx))
  fDerivgInt gDerivfInt lim_at_zero lim_at_inf
State after:
no goals