## 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: May 12 2021 at 08:14 UTC