Mathlib has `-x * log x` and some things on entropy

[adomasbaliuka]

Maybe you're already aware or don't want to constantly update how Mathlib is used, but some of the things in your repo are already in Mathlib. For example some of the things here:

Lean-QuantumInfo/ClassicalInfo/Entropy.lean

Line 15 in aed3615

def H₁ : Prob → ℝ :=

are at Mathlib.Analysis.SpecialFunctions.Log.NegMulLog.

I defined binary entropy (which maybe you don't need explicitly) which will be merged soon here

and there is measure-theoretic entropy which maybe will get merged eventually here

[Timeroot]

Hi Adomas,

Yes, thanks! I had noticed the thread on the Zulip about the entropy. :) I hadn't been working very much on this for the past couple of months, and I've "fallen behind" Mathlib on a few things. I'm getting a bit more time now for this, I'm currently trying to get back up to speed, and then see what things in Mathlib I can pull in / what I can upstream back into Mathlib (because I have some useful lemmas too, I think).

I see that your binary entropy function was merged 4 days ago, too! (I don't know why GitHub didn't let me know about your comment here until now...) I'll try to take a look at integrating better soon. :)