rw [MellinTransform_eq, MellinInverseTransform_eq, mellin_inversion σ f hx hf hFf hfx]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℝ → ℂ
x : ℝ
hx : 0 < x
hf : MellinConvergent f ↑σ
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
⊢ MellinInverseTransform (𝓜 f) σ x = f x
no goals