Zulip Chat Archive

Stream: maths

Topic: Integration


view this post on Zulip Patrick Massot (Jul 04 2019 at 11:41):

It seems mathlib now has some kind of integration. But I'm don't understand the details. For instance, how far are we from computing 01xdx\int_0^1 x\,dx? What kind of big theorems do we have?

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:50):

The Bochner integral has been defined. The big theorem is that the integral exists

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:50):

We have yet to show that it is linear, etc

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:50):

but that shouldn't be very hard given the facts we have about dense embeddings

view this post on Zulip Mario Carneiro (Jul 04 2019 at 11:51):

We have nothing on real integrals


Last updated: May 12 2021 at 08:14 UTC