Gaussian integral

Stream: maths

[Anatole Dedecker]

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).

[Bryan Gin-ge Chen]

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

[Patrick Massot]

@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).

[Patrick Massot]

@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.

[Kevin Buzzard]

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

[Yury G. Kudryashov]

A few comments:

• continuous_linear_map.continuous_apply: we have a bundled docs#continuous_linear_map.apply;
• I used (∀ x, integrable_at_filter f (nhds x) mu) instead of loc_integrable, see docs#measure_theory.integrable_at_filter and docs#is_compact.integrable_on_of_nhds_within;
• for interval integrals you can either introduce interval_oc and lemmas as in your file or use something like wlog hle : a ≤ b. Unfortunately, it feels more painful than it should either way.