apply setIntegral_congr_ae measurableSet_Ioi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∫ (x : ℝ) in Ioi 0, DeltaSpike Ψ ε x / x =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 → DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))