measurability of special functions

Stream: maths

[Yury G. Kudryashov]

I'm formalizing measurability of exp, log, etc. Where should it go?

[Yury G. Kudryashov]

@Sebastien Gouezel @Floris van Doorn What do you think?

[Yury G. Kudryashov]

Should I create a new file or make analysis/calculus/special_functions/* depend on borel_space?

[Yury G. Kudryashov]

Another question: what do you think about adding typeclasses has_measurable_(mul/add/neg/div/sub/coe)? Currently a user has to choose, e.g., between measurable.mul and measurable.ennreal_mul.

[Sebastien Gouezel]

Yury G. Kudryashov said:

Should I create a new file or make analysis/calculus/special_functions/* depend on borel_space?

No strong opinion on this. I would probably let the files depend on borel_space and add measurability statements just after the continuity statements for each function.

[Patrick Massot]

Same here.

[Floris van Doorn]

Same here. I like Sebastien's suggestion.

About the has_measurable_* typeclasses, I'm wondering whether we should directly mimic the topological algebraic structures:
has_measurable_mul, measurable_group (instead of has_measurable_div and has_measurable_inv) and maybe measurable_ring.
has_measurable_coe would be nice, I guess, so that you don't have to specify which coercion in measurable, but I don't think it's too important.

[Yury G. Kudryashov]

I prefer has_measurable_sub because we'll have instances, e.g., for ennreal and nat.

[Yury G. Kudryashov]

Similarly for has_measurable_div

[Yury G. Kudryashov]

And I don't want to extend algebraic classes here to avoid difficulties with assumptions like [topological_add_monoid A] [has_sub A] [has_measurable_sub A]

[Floris van Doorn]

Ok, that's also fine by me.