[Merged by Bors] - feat(analysis/special_functions/gaussian): formula for gaussian integrals

[sgouezel]

---

• depends on: [Merged by Bors] - chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas #15117
• depends on: [Merged by Bors] - feat(topology/sets/compacts): prod constructions #15118
• depends on: [Merged by Bors] - feat(linear_algebra): basis on R × R, and relation between matrices and linear maps in this basis  #15119
• depends on: [Merged by Bors] - feat(measure_theory/group/measure): a product of Haar measures is a Haar measure #15120
• depends on: [Merged by Bors] - feat(analysis/special_functions/polar_coord): define polar coordinates, polar change of variable formula in integrals #15258

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas #15117
• [Merged by Bors] - feat(topology/sets/compacts): prod constructions #15118
• [Merged by Bors] - feat(linear_algebra): basis on R × R, and relation between matrices and linear maps in this basis  #15119
• [Merged by Bors] - feat(measure_theory/group/measure): a product of Haar measures is a Haar measure #15120
• [Merged by Bors] - feat(analysis/special_functions/polar_coord): define polar coordinates, polar change of variable formula in integrals #15258
  By Dependent Issues (🤖). Happy coding!

[ADedecker]

LGTM

Do you think it would be possible to avoid some of the integrability proofs by using nnreal valued functions ? Or are all of them useful anyway ?

[sgouezel]

I think the integrability statements are good to have anyway, so I haven't tried to avoid them.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests