apply setIntegral_eq_zero_of_forall_eq_zero
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
⊢ ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then DeltaSpike Ψ ε (x / y) else 0) / y = 0
case h.right.ht_eq
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
⊢ ∀ x_1 ∈ Ioi 0, (if 0 < x_1 ∧ x_1 ≤ 1 then DeltaSpike Ψ ε (x / x_1) else 0) / x_1 = 0