norm_cast
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑(t * Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume