# Zulip Chat Archive

## Stream: maths

### Topic: integrals

#### Patrick Massot (Jun 22 2020 at 09:40):

I'm trying to start using integrals in mathlib, and I don't understand the type of the definition. `#check @measure_theory.integral`

says:

```
measure_theory.integral :
Π {α : Type u_3} [_inst_1 : measure_theory.measure_space α] {β : Type u_4} [_inst_2 : normed_group β]
[_inst_3 : topological_space.second_countable_topology β] [_inst_4 : normed_space ℝ β]
[_inst_5 : complete_space β] [_inst_6 : measurable_space β] [_inst_7 : borel_space β], (α → β) → β
```

#### Patrick Massot (Jun 22 2020 at 09:40):

Why do we need a measurable space structure on the target? @Sebastien Gouezel do you understand that?

#### Sebastien Gouezel (Jun 22 2020 at 09:54):

To integrate a function, it has to be measurable. Which means that you need sigma-algebras both in the source space and in the target space. In the target space, you have the Borel sigma algebra, but we do not register as an instance that a topological space is always endowed with a measurable structure which is the Borel sigma algebra, because sometimes it is not the right thing to do (for instance, it is pretty common to work with the completion of the Borel sigma algebra with respect to some measure). Instead, you should assume that you have a sigma algebra, and in the situation you are considering you want it to be the Borel sigma algebra, which is what `borel_space β`

says.

If I recall correctly, it was not like that at the start, but the initial setup (where topological spaces have by defaults the borel sigma algebras) created countless problems, and it was refactored by Yury to be like that.

#### Patrick Massot (Jun 22 2020 at 09:57):

Ok, what's the user manual then? Should I have variables saying everybody is `borel_space`

or a local instance declaration?

#### Patrick Massot (Jun 22 2020 at 09:57):

My target space is a finite dimensional real vector space.

#### Sebastien Gouezel (Jun 22 2020 at 10:04):

I would put it in the `variables`

declaration. Maybe @Yury G. Kudryashov will know better.

#### Yury G. Kudryashov (Jun 22 2020 at 19:59):

You should assume `measurable_space`

and `borel_space`

.

#### Yury G. Kudryashov (Jun 22 2020 at 20:16):

The main reason for the refactor was that with the old setup it was impossible to say "we have `[topological_space α]`

and `[measure_space α]`

and they agree on `[measurable_space α]`

". Another reason is diamonds: we have `[measurable_space]`

instances on `nat`

etc and they are not defeq `borel`

. Moreover, this can't be solved by the "forgetful inheritance" trick because for `α×β`

two constructions agree only if you require some countability from topologies.

Last updated: May 06 2021 at 19:30 UTC