new lemmas for infotheo

[hoheinzollern]

Dear infotheo authors, I want to point out that my co-authors and I have a paper on the formalization of bounds on the trimmed mean algorithm that uses infotheo. It has been accepted at PPDP this year (https://ppdp2021.github.io/#accepted, the paper is called "Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation", soon to be available) and you can find the source code of the formalization here: https://github.com/ieva-itu/robustmean/blob/main/robustmean.v

We are thankful for the all the development of probability theory that we used in our paper, and we think you might appreciate some lemmas that should belong to infotheo more than our development.
As we are all novice Coq programmers and not used to the mathcomp style, I'd appreciate if you could take a look at the code and see whether you're interested in integrating it here, and maybe help us match the style of the infotheo package. This is also why I'm not making a pull request yet.

[affeldt-aist]

Congratulations! I'm looking forward to reading your paper.
We are interesting in integrating it and I am willing to spend time on it.
Maybe the easiest way is to PR so that we can exchange about the code.

[hoheinzollern]

Sounds great, and thanks for the offer!
I'll mention here my colleagues @ieva-itu and @carstenschuermann so they are in the loop.
We'll start a pull request soon.

[t6s]

@hoheinzollern
I can help modifying the proof script into a more mathcomp-ish style.
Do you prefer such a change?

[hoheinzollern]

That would be very appreciated, of course I'd like to learn in the process if possible :)
Could we do this together?