Integration on ℝ by parts

Stream: Is there code for X?

[Aaron Bies]

I have a problem of the form ∫ (x : ℝ), x * f x and would like to solve it using integration by parts.

The relevant theorem seems to be interval_integral.integral_mul_deriv_eq_deriv_mul, but I need some way to turn my integral into one with interval bounds, so something like:

∫ (x : ℝ), f x = lim N → ∞, ∫ x in -N .. N, f x

Does this lemma exist somewhere or is there a variation of integration by parts I can use here?

[Sebastien Gouezel]

See docs#measure_theory.interval_integral_tendsto_integral

[Sebastien Gouezel]

In this file, we also have versions of integration by parts on semiinfinite intervals, but not on the whole line as far as I can tell. It's not that there is any difficulty here, only that no one has needed it yet.

[Aaron Bies]

Actually, what would be a good way to show that λ x, x * f x is integrable, if I already know f is?

It seems measure_theory.integrable.bdd_mul is almost what I want, but it requires me to prove that λ x, ‖x‖ either has an upper bound or a finite integral.

[Jireh Loreaux]

It's not true. Take f x := 1 / x ^ 2.

[Kalle Kytölä]

I think Jireh meant f(x)=1/(1+x^2) so f is integrable, but indeed the statement is just not true.

[Aaron Bies]

I will rephrase the question:

If you ever computed the expected value of a random variable using its pdf, you will be familiar with integrating functions of the form λ x, x * f x. I want to do just that, but it seems most theorems about integrals in mathlib also require a proof that the function is integrable in the first place. While trying to write that proof, I was only able to find a single theorem about multiplication in mathlib, that being measure_theory.integrable.bdd_mul, which isn't applicable because of the left-hand side. Is there something I can use in this situation?

[Yaël Dillies]

Are you following a paper proof that we can have a look at? What's the pdf in question?

[Aaron Bies]

The pdf in question is the normal distribution

[Aaron Bies]

It is (more or less) this proof

[Yaël Dillies]

@Jason KY., you will know the optimal way of proving this.

[Jireh Loreaux]

@Aaron Bies just so you're aware, some distributions have "heavy tails", which means they're expectation is infinite (i.e., the integrand in your question is not integrable). This doesn't apply to the normal distribution, but it does in general.

[Kalle Kytölä]

Aaron Bies said:

It is (more or less) this proof

Like many informal proofs, this proof doesn't bother the reader with the fully detailed justifications for the use of the fundamental theorem of calculus. It assumes that the reader is able to fill in some needed integrability assumptions. But in order to write a formal proof, you will need to provide also those omitted justifications.

As you said, the integration by parts theorem docs#interval_integral.integral_mul_deriv_eq_deriv_mul is a key result, and results of the flavor docs#measure_theory.interval_integral_tendsto_integral are needed then to get to the whole real line as Sébastien said. In that step, you probably need to prove something to the effect that $x \mapsto x e^{-x^2/2}$ is integrable. This should not be difficult --- but to convince yourself that it is not automatic, recall Jireh's warning that it is wrong for general $x \mapsto x f(x)$ even if $f$ itself is integrable.

[Kalle Kytölä]

The (modified) Jireh's warning can be modified to illustrate the the proof you linked to does some reasoning not made explicit in it. If we set $f(x) = \frac{1}{\pi} \frac{1}{1+x^2}$ (the density of the Cauchy distribution), then a primitive of $x f(x)$ is $\frac{1}{2\pi} \log(1+x^2)$. Do we have "by fundamental theorem of calculus" (as in the proof you quote):

$$\int_\R x f(x) \, dx \overset{?}{=} \Big[ \frac{1}{2\pi} \log(1+x^2) \Big]_{-\infty}^{+\infty} \; ?$$

[Jason KY.]

We do have measure_theory.pdf.integral_mul_eq_integral which might be what you are looking for?