Integral_infty

Stream: new members

[Parivash]

Hi,
Can we prove this integral by lean?
$\int_{0}^{\infty}x^{2n}exp(-\frac{x^2}{a^2})dx=\sqrt \pi \frac{(2n)!}{n!}(\frac{a}{2})^{2n+1}$

[Jason Rute]

I would be curious to know the answer to this, just to see how far calculus has come in Lean. I doubt mathlib has this exact integral, but the proof I believe is induction starting with the Guassian integral as the base case and then repeated integration by parts. (I haven't worked out the details to be sure.)

• It looks like the Gaussian integral was just added (and it is stated over the whole real line): docs#integral_gaussian
• Lean seems to have integration by parts (for interval integrals at least): docs#interval_integral.integral_deriv_mul_eq_sub
• Lean has a proof that the (complex) Gamma function equals the factorial on natural numbers (which uses a similar induction w/ integration by parts proof if I'm not mistaken): docs#complex.Gamma_nat_eq_factorial

[Ruben Van de Velde]

A good first step would be to state the lemma as a #mwe

[Moritz Doll]

The crucial point is integration by parts. This certainly can be done by hand using integration by parts for interval (the meat of the proof Jason mentioned is in docs#complex.Gamma_integral_add_one ), but the more structured approach would be to prove integration by parts for Schwartz functions

[Parivash]

@Jason Rute
Thank you Jason for providing useful links, I'll look at them. As I reach a result I will inform you