independence, expectation of product

[affeldt-aist]

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

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

[affeldt-aist]

Maybe it is better to rename expectation_prod to expectation_mul since the original intent was expectationM.

[t6s]

I have reviewed lines 0 -- 878 and quickly looked through 879-.
The latter things need some cleaning.

[t6s]

I forgot the context for this draft PR. What is the current status?

[affeldt-aist]

I forgot the context for this draft PR. What is the current status?

Rebased but for reasons I forgot some things look duplicated in probability.v and independence.v.
If I remember correctly, we introduced definitions of independence following Klenke's book and
were able to reproduce a few, non-trivial lemmas.
What about we remove duplications and PR only an independence.v file with what we have so far?
(That would save me the trouble of regular rebasings and certainly these definitions will be wanted at some point.)

[affeldt-aist]

I removed duplicates and unused lemmas and did some cleaning.
@t6s About the status: I think that this PR is really proposing definitions and justifying them with standard theorems from the literature.
If one finds it useful to have these definitions in master we can maybe think of merging at some point after review with some "experimental" proviso in the header file (like we did in the past for probability.v).
What do you think @hoheinzollern ?
fyi: @CohenCyril @proux01

[t6s]

This lemma should be removed as it is just an instance of funrposneg above.

[t6s]

This one, on the other hand, is nontrivial and should be kept.

[t6s]

But the name looks bad and I have no good suggestion for now.

[t6s]

funrD_posBneg would be better.

This can be seen as a form of distributivity where ^\+ and ^\- parallelly distributes over \+ inside
expressions of the form _^\+ \- _^\-. I do not know how to name it.

[affeldt-aist]

In fact this lemma has a short proof once one observes that it almost corresponds to interchange with addition and subtraction (most if not all uses of interchange in MathComp use twice the same operator). interchange lemmas are suffixed with ACA like addrACA but that might be an overkill here to abide by this naming scheme because we mix two operators and moreover on functions (calling for a fctE suffix) so maybe addBr could be enough to suggests interchange sub add and therefore the name could just be funrDB (and funeDB for the corresponding lemmas for extended real numbers).

[t6s]

interchange is indeed another structure involved here, and I also thought about incorporating ACA in its name, though not coming up with a tidy result.

funrDB is neat but looks a bit too stripped off since it does not clearly indicate that it is about ^+ and ^-.
I am however not sure how to restore that info without elongating the name, and weakly approving funrDB.

[t6s]

I have reviewed lines 0 -- 878 and quickly looked through 879-. The latter things need some cleaning.

It looks like I reviewed independence.v once, and the file looks not so bad. @hoheinzollern can you double check?

I have read the other files and put some comments requesting some changes.

[affeldt-aist]

I have read the other files and put some comments requesting some changes.

Thanks for the comments that triggered very welcomed improvements.

[CohenCyril]

why is measurability built in independence of variables? I would have expected measurability to be a side condition. (Same remark in each definition below)