exact integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin.mp this |>.1
case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
this : IntegrableOn (fun x => x ^ (r / 2 - 1)) (Ioi ↑N) volume
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume
no goals