New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: integration by parts on the whole real line, assuming integrability of the product #11916
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
bors d+
on `(a, +∞)` and continuity at `a⁺`. | ||
|
||
Note that such a function always has a limit at infinity, | ||
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm wondering if we should just make the RHS of this limUnder atTop f - f a
, and then ensure we have simp
-lemmas that can compute limUnder
. Not for this PR though.
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…lity 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.
Pull request successfully merged into master. Build succeeded: |
…lity 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.
…lity 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.
…lity 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.
…lity 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.
We already have that
∫ (x : ℝ), u x * v' x = b' - a' - ∫ (x : ℝ), u' x * v x
ifu * v
tends toa'
andb'
at minus infinity and infinity. Assuming morevoer thatu * v
is integrable, we show that it tends to0
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.The advantage of the version with global integrability is that it generalizes readily to higher dimensional spaces (forthcoming PR, and then applications for the Fourier transform).