apply LocallyIntegrableOn.integrableOn_of_isBigO_atTop (g := fun x ↦ x ^ (r / 2 - 1))
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume
case hf
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ LocallyIntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume

case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)

case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume