unfold Smooth1 DeltaSpike MellinConvolution
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => Smooth1 ψ ε x
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x =>
    ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (fun x => ψ (x ^ (1 / ε)) / ε) (x / y) / ↑y