Zulip Chat Archive

Stream: maths

Topic: Gaussian measure


view this post on Zulip Kevin Buzzard (Oct 02 2018 at 17:09):

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

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 17:15):

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.

view this post on Zulip Reid Barton (Oct 02 2018 at 17:19):

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

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 17:23):

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

view this post on Zulip Johan Commelin (Oct 02 2018 at 17:33):

We don't have derivatives yet, do we?

view this post on Zulip Chris Hughes (Oct 02 2018 at 17:34):

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

view this post on Zulip Mario Carneiro (Oct 02 2018 at 17:42):

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

view this post on Zulip Patrick Massot (Oct 02 2018 at 18:46):

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


Last updated: May 10 2021 at 08:14 UTC