Zulip Chat Archive

Stream: maths

Topic: Gaussian integral


view this post on Zulip Anatole Dedecker (Feb 27 2021 at 21:16):

A few weeks ago, I wanted to experiment with the API for integrals in mathlib, and I thought the best way to do that would be to use it to prove something not trivial but reasonably easy. So here is a proof of the Gaussian integral (∫ x : ℝ, real.exp (-x^2) = real.pi.sqrt) : https://github.com/ADedecker/gauss/blob/master/src/main.lean#L336
As I couldn't find variable change in 2D in mathlib, I didn't make the usual proof, and I used parametric integrals instead.

The only sorry remaining will be removed once #6292 gets merged.

I don't know wether this should go to mathlib or not, but the main.lean file is definitely not PR-ready. I will do a lot of cleaning and a bit of generalizing soon, but right now I have more urgent things to do. Also, for lemmas about parametric integrals, it may be better to adapt what @Patrick Massot did in the Sphere Eversion project, since it should give results a bit more general than what I took from the undergraduate course I attended last semester :sweat_smile:

The integral_limits.lean file seems a bit closer to being PR-able, but I'm still not happy with some details of it, so feel free to have a look and give your opinions.

PS : Big thanks to the authors of the measure theory part of mathlib for having made an API understandable even by people like me who don't know measure theory (yet).

view this post on Zulip Bryan Gin-ge Chen (Feb 27 2021 at 21:23):

Great job! We'll certainly want this result in mathlib eventually, even if you decide not to PR your work in its current form.

view this post on Zulip Patrick Massot (Feb 28 2021 at 15:04):

@Anatole Dedecker I just bumped mathlib in the sphere eversion project. I hope I'll able to PR everything I have about parametric integrals before the end of the week, but you can already copy https://github.com/leanprover-community/sphere-eversion/blob/master/src/parametric_integral.lean wherever you want and play with it using mathlib master (it doesn't depend on any other sphere eversion file).

view this post on Zulip Patrick Massot (Feb 28 2021 at 15:08):

@Yury G. Kudryashov @Sebastien Gouezel @Floris van Doorn it would also be great if you could have a look at that file before I slice it into PRs. You can dump it into you current mathlib and have a look. Note that the most painful part is around interval_integral, I'd love to learn what I'm meant to do there.

view this post on Zulip Kevin Buzzard (Feb 28 2021 at 16:03):

@Ryan Lahfa the sphere eversion project would be a fabulous summer project to work on

view this post on Zulip Yury G. Kudryashov (Mar 02 2021 at 00:22):

A few comments:


Last updated: May 09 2021 at 09:11 UTC