theorem needed for integration

Stream: new members

[Joy Hu]

Hi, everyone. Sorry for the stupid questions. I am trying to prove something related to gaussian measure in Lean and thus I need a lot of theorems to evaluate the integration parts. Someone has told me gaussian_integral, which is quite useful. But I still need some other theorems. My first question is that suppose that I have ∫ (x : ℝ), x * exp (-x ^ 2), is there any way that I can evaluate this in lean?

[Joy Hu]

Screenshot-2022-08-13-at-17.06.18.png

[Joy Hu]

I wanna do some calculations like the above picture in lean and then show that this tends to zero. I looked for some useful lemmas in the Mathlib but failed. Are there any tricks that can apply when we trying to find some particular things in the Mathlib? So hard to find an appropriate theorem in Mathlib :sob:

[Junyan Xu]

I think you'd want to look into the files
https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/interval_integral.html and
https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/integral_eq_improper.html

[Joy Hu]

Thank you! I will have a look on these files