Has Entropy been upstreamed to Mathlib

Stream: Polynomial Freiman-Ruzsa conjecture

[Shreyas Srinivas]

Hello, I am looking for the definition of entropy of a distribution which I found here. I wanted to ask if this definition has already reached Mathlib, and if so, under what name?

[Shreyas Srinivas]

I really only need basic facts about entropy such as concavity. I just need it on an arbitrary distribution on a finite set.

[Shreyas Srinivas]

Alternatively, if I use this project's definitions and theorems on entropy, is it advisable to use it as a dependency of just borrow the relevant definitions and attribute them in a doc comment?

[Shreyas Srinivas]

Specifically this definition : https://github.com/teorth/pfr/blob/0d9c5da9388d34d3b4c591f28f4e206e678817b3/PFR/ForMathlib/Entropy/Basic.lean#L43-L45

[Rémy Degenne]

It's not in Mathlib. However we have the Kullback-Leibler divergence in Mathlib (InformationTheory.klDiv), from which you can build the entropy if you want. Not that it's much easier than defining an entropy directly, but you could reuse a lemma or two.

[Shreyas Srinivas]

In my case I want to work on purely discrete probability spaces.

[Shreyas Srinivas]

KL divergence seems one step removed from entropy. Is it convenient to use for proofs where I would probably not compare distributions?

[Shreyas Srinivas]

Rémy Degenne said:

It's not in Mathlib. However we have the Kullback-Leibler divergence in Mathlib (InformationTheory.klDiv), from which you can build the entropy if you want. Not that it's much easier than defining an entropy directly, but you could reuse a lemma or two.

I am wondering about that for basically most probability theory. On the one hand, reinventing the wheel seems tedious. On the other hand I want to keep the measure theoretic probability ideas as deeply hidden as I can, even in proofs. For example, if I need to prove a fresh concentration bound, should I set it up in measure theoretic lingo or should I set it up in the discrete form that I am more fluent with by a lot (I work in CS theory largely).

[Shreyas Srinivas]

I might end up learning/re-learning enough measure theory to not worry about this if I stick with higher abstraction, but I don’t know if that is the optimal way to get the job done.