Zulip Chat Archive

Stream: maths

Topic: integrals


view this post on Zulip 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 β], (α  β)  β

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 22 2020 at 09:57):

My target space is a finite dimensional real vector space.

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 10:04):

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

view this post on Zulip Yury G. Kudryashov (Jun 22 2020 at 19:59):

You should assume measurable_space and borel_space.

view this post on Zulip 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