Commit 2024-04-05 23:03 9db18cff

feat: integration by parts on the whole real line, assuming integrability of the product (#11916) We already have that ∫ (x : ℝ), u x * v' x = b' - a' - ∫ (x : ℝ), u' x * v x if u * v tends to a' and b' at minus infinity and infinity. Assuming morevoer that u * v is integrable, we show that it tends to 0 at minus infinity and infinity, and therefore that ∫ (x : ℝ), u x * v' x = - ∫ (x : ℝ), u' x * v x. We also give versions with a general bilinear form instead of multiplication.