Commit 2025-05-30 09:57 478adcbe

feat(Analysis): Integrability of shifted power function (#25045) add a generalization of integrableOn_Ioi_rpow_of_lt proving the integrability of (fun t : ℝ ↦ (t + m) ^ a) on (c, ∞) for all 0 ≤ m, a < -1 and 0 < c.