∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (σ : ℝ) (f : ℂ → E) (x : ℝ),
  mellinInv σ f x = (1 / (2 * Real.pi)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * Complex.I)) • f (↑σ + ↑y * Complex.I)