In the current formulation of measure theory and integrals, we have measurable spaces but not measure spaces
(measure space = measurable space bundled with a measure).
This shortage, combined with an automatic choice of a default measure, seems to be leading to an embarrassing glitch:
#math-comp analysis > Fail of `integral_set1`
(Thanks for spotting and reporting, @Yosuke-Ito-345 )
It would be nice to have the measure space structure to avoid this kind of issues and also to make the notation for integrals simpler.
(When formalizing it, it would be worth considering also the notion of enhanced measurable space:
https://ncatlab.org/nlab/show/categories+of+measure+theory#enhanced_measurable_spaces )
In the current formulation of measure theory and integrals, we have measurable spaces but not measure spaces
(measure space = measurable space bundled with a measure).
This shortage, combined with an automatic choice of a default measure, seems to be leading to an embarrassing glitch:
#math-comp analysis > Fail of `integral_set1`
(Thanks for spotting and reporting, @Yosuke-Ito-345 )
It would be nice to have the measure space structure to avoid this kind of issues and also to make the notation for integrals simpler.
(When formalizing it, it would be worth considering also the notion of enhanced measurable space:
https://ncatlab.org/nlab/show/categories+of+measure+theory#enhanced_measurable_spaces )