Theorem: MellinInversion_aux3 (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
σ : ℝ
σ_ne_zero : σ ≠ 0
σ_ne_negOne : σ ≠ -1
fInt : IntegrableOn (fun x => f x * ↑x ^ ↑σ) (Ioi 0) volume
⊢ IntegrableOn
    (fun x =>
      match x with
      | (x, t) => f x * ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1)))
    ((Ioi 0).prod univ) volume
Tactic:
sorry
State after:
no goals