Topic: Gaussian integral
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.
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:
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 (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.
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).
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.
Kevin Buzzard (Feb 28 2021 at 16:03):
@Ryan Lahfa the sphere eversion project would be a fabulous summer project to work on
Yury G. Kudryashov (Mar 02 2021 at 00:22):
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_ocand lemmas as in your file or use something like
wlog hle : a ≤ b. Unfortunately, it feels more painful than it should either way.
Last updated: May 09 2021 at 09:11 UTC