integrals

Stream: maths

[Patrick Massot]

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]

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

[Sebastien Gouezel]

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]

Ok, what's the user manual then? Should I have variables saying everybody is borel_space or a local instance declaration?

[Patrick Massot]

My target space is a finite dimensional real vector space.

[Sebastien Gouezel]

I would put it in the variables declaration. Maybe @Yury G. Kudryashov will know better.

[Yury G. Kudryashov]

You should assume measurable_space and borel_space.

[Yury G. Kudryashov]

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.