Integration by parts on infinite intervals

Stream: Is there code for X?

[Alex Kontorovich]

We have intervalIntegral.integral_mul_deriv_eq_deriv_mul which is integration by parts on finite intervals, and we have MeasureTheory.intervalIntegral_tendsto_integral_Ioi that integrals on infinite intervals are limits of finite ones. Am I correct that there's currently no API seamlessly connecting the two? (So one should do it manually...? Or perhaps develop the API...?)

[Floris van Doorn]

We should definitely develop API for that.

[Moritz Doll]

#10099

[Moritz Doll]

for integrals over the reals