# Zulip Chat Archive

## Stream: maths

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

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 (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_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.

Last updated: May 09 2021 at 09:11 UTC