refine mellin_differentiableAt_of_isBigO_rpow (a := 1) (b := -1) ?_ ?_ (by simp) ?_ (by simp)
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ DifferentiableAt ℂ (mellin fun x => ↑(Ψ x)) ↑0
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ LocallyIntegrableOn (fun x => ↑(Ψ x)) (Ioi 0) volume

case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[atTop] fun x => x ^ (-1)

case h.refine_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun x => ↑(Ψ x)) =O[𝓝[>] 0] fun x => x ^ (- -1)