dsimp [DeltaSpike]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ DeltaSpike Ψ ε x
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
x ε : ℝ
xpos : 0 < x
εpos : 0 < ε
⊢ 0 ≤ Ψ (x ^ (1 / ε)) / ε