Theorem: MellinInversion (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : 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
Tactic:
rw [MellinTransform_eq, MellinInverseTransform_eq, mellin_inversion σ f hx hf hFf hfx]
State after:
no goals