Zulip Chat Archive

Stream: maths

Topic: Integration

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 $\int_0^1 x\,dx$ ? What kind of big theorems do we have?

Mario Carneiro (Jul 04 2019 at 11:50):

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

Mario Carneiro (Jul 04 2019 at 11:50):

We have yet to show that it is linear, etc

Mario Carneiro (Jul 04 2019 at 11:50):

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

Mario Carneiro (Jul 04 2019 at 11:51):

We have nothing on real integrals

Last updated: Dec 20 2023 at 11:08 UTC