[lyonel2017]

Motivation for this change

Provide a connection between esum and lesbegue_integrale (extracted from #2049).

Depends on #2062.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

PR #2062 merged -> need rebasing

[lyonel2017]

PR #2062 merged -> need rebasing

I made a rebase.

[affeldt-aist]

Thanks for the rebase!

[affeldt-aist]

Note that this PR has clamp but does not actually use it, it can be removed since moreover it is the target of another PR.

[lyonel2017]

Note that this PR has clamp but does not actually use it, it can be removed since moreover it is the target of another PR.

This PR is now rebase on top of master.

[affeldt-aist]

@lyonel2017 where do you use discrete_measurable_space in your developments? for the record, I would like to keep a pointer to a clear application for potential users. (A pointer inside #2116 could be enough.)

(I took the liberty to adapt naming to the rest of the library, trying to preserve consistency as much as possible still taking your proposals into account, do not hesitate to share concerns if any.)

[lyonel2017]

@lyonel2017 where do you use discrete_measurable_space in your developments? for the record, I would like to keep a pointer to a clear application for potential users. (A pointer inside #2116 could be enough.)

I made a small experiment in the context of #2116 to check that the definition of expectation of #2064 and from random_variable.v are the same : expectationE. I'm not sure if this is the best approach for this proof.

[hoheinzollern]

See comments above.

[affeldt-aist]

In the last commit, I essentially removed the mention to measurable_space from the header (it does not seem to exist), add a bit of documentation, and use infinite_esum_cst (generalized as suggested @hoheinzollern) to simplify the proof in counting_measure.v.

[affeldt-aist]

(I think that @hoheinzollern have all been addressed: thanks for the careful review!)