Gaussian measure

Stream: maths

[Kevin Buzzard]

Today the subject of formalising Gaussian measure in Lean came up at work. I asked Johannes about it privately and he seemed optimistic that it was within reach. But then he mentioned some work done at Dagstuhl on the Lebesgue integral which is...possibly not accessible at this point? @Mario Carneiro do you have access to this stuff and is it in any state to be made public? As Patrick has pointed out in the past, our analysis is weak in places, and this probably simply because us number theorists / geometers are working on our pet projects where a bunch of foundational stuff has been done already, whereas any potential analysts will soon discover that there are still gaps in the coverage of 1st year undergraduate analysis (did anyone do the product rule yet??).

[Kevin Buzzard]

I guess we'll also need $\pi$ :-) Did it make it into mathlib yet? I glanced through recent commits and PRs and couldn't spot it.

[Reid Barton]

You mean the product rule for the formal derivative of polynomials?

[Kevin Buzzard]

heh, no, for differentiable functions $\mathbb{R}\to\mathbb{R}$ :-)

[Johan Commelin]

We don't have derivatives yet, do we?

[Chris Hughes]

No. There is something called polynomial.derivative or something, just for polynomials without mentioning analysis.

[Mario Carneiro]

Here's the integration file, which I've pushed to community mathlib: https://github.com/leanprover-community/mathlib/commit/10e3f42dc73fa9148e0f1847f6201bc608aa2488

[Patrick Massot]

It looks like a good start. Let's hope algebra will soon leave you some time for working on this