calc
  _ = ∫ (y : ℝ) in Ioi 0, indicator (Ioc 0 1) (fun y ↦ DeltaSpike Ψ ε (x / y) / ↑y) y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y := ?_
  _ = _ := integral_comp_div_I0i_haar (fun y ↦ DeltaSpike Ψ ε y) xpos
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y

case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y =
    ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y