Adds measurable_expR and measurable function composition

[hoheinzollern]

Measurable function composition only works in the specific case where f and g are maps to reals

Motivation for this change

Required lemmas for #1053

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[hoheinzollern]

I looked into generalizations of measurable function composition, and indeed two measurable functions do not necessarily compose into a measurable function. This article gives a few conditions upon which the composition of measurable functions is measurable. Should we implement some of those as well?
This stackoverflow question is also relevant: https://math.stackexchange.com/questions/283443/is-composition-of-measurable-functions-measurable
@affeldt-aist @CohenCyril

[affeldt-aist]

If I am not mistaken, the changes proposed by this PR somehow already made their way into master.
I therefore propose to close.
@hoheinzollern Do you want to record your references about the composition of measurable functions in an issue with labels such as with/help wanted/questions?

[affeldt-aist]

If I am not mistaken, the changes proposed by this PR somehow already made their way into master. I therefore propose to close. @hoheinzollern Do you want to record your references about the composition of measurable functions in an issue with labels such as with/help wanted/questions?

ping @hoheinzollern ?

[hoheinzollern]

It looks indeed like the issue has been addressed in master, I'm happy to have it closed