Commit 2023-12-20 19:25 051aa734

feat: non-integrability results of derivatives on [a, +oo) (#8712) We have in the library the lemma not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter, saying that if a function tends to infinity at a point in an interval [a, b], then its derivative is not interval-integrable on [a, b]. We generalize this result to allow for any set instead of [a, b], and apply it to half-infinite intervals. In particular, we characterize integrability of x^s on [a, +oo), and deduce that x^s is never integrable on [0, +oo). This makes it possible to remove one assumption in Lemma mellin_comp_rpow on the Mellin transform.