apply DifferentiableAt.differentiableWithinAt
𝕂 : 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
⊢ DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
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 ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) 0