## Stream: maths

### Topic: measurability of special functions

#### Yury G. Kudryashov (Sep 28 2020 at 05:57):

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

#### Yury G. Kudryashov (Sep 28 2020 at 05:57):

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

#### Yury G. Kudryashov (Sep 28 2020 at 05:58):

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

#### Yury G. Kudryashov (Sep 28 2020 at 06:00):

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 (Sep 28 2020 at 07:05):

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.

Same here.

#### Floris van Doorn (Sep 28 2020 at 19:06):

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 (Sep 28 2020 at 19:09):

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

#### Yury G. Kudryashov (Sep 28 2020 at 19:09):

Similarly for has_measurable_div

#### Yury G. Kudryashov (Sep 28 2020 at 19:10):

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 (Sep 28 2020 at 19:29):

Ok, that's also fine by me.

Last updated: May 06 2021 at 18:20 UTC