Upstream to Mathlib

Stream: Polynomial Freiman-Ruzsa conjecture

[Pietro Monticone]

Opened #18034.

[Daniel Weber]

I want to use entropy in Mathlib, how can I help with upstreaming the relevant parts from PFR?

[Yaël Dillies]

The answer is to not upstream from PFR, but rather from TestingLowerBounds

[Yaël Dillies]

Because @Rémy Degenne and @Lorenzo Luccioli are also upstreaming at the same time, I am currently working on improvements to my upstreaming dashboard so that it automatically tells me all PRs to mathlib that touch a file I could upstream

[Rémy Degenne]

Our project contains a definition and properties of the Kullback-Leibler divergence, from which you can get entropy, but it is also in the middle of a complete overhaul that changes most definitions including KL. It changes more than 10000 lines and has many sorry left so don't count on us upstreaming soon.

Also Mathlib might want an entropy definition with a tsum anyway, tailored to the discrete case. So we could PR from PFR without waiting for the TestingLowerBounds project.

[Rémy Degenne]

I have opened a PR for the Kullback-Leibler divergence: #21053 .
I still think that we also want a more direct definition for the discrete entropy (and we'll link the two definitions afterwards), so upstreaming from PFR is still a good idea.

[Yaël Dillies]

Interesting. What makes you think we want the direct definition? And do we want the direct definition from PFR before or after the introduction of FiniteRange?

[Rémy Degenne]

The KL definition is now merged to Mathlib.
I forgot to answer the last question from Yaël Dillies: after thinking about it more, I'm not really sure about it. I supposed that for probability over finite types (I wrote discrete above but I was really thinking finite) we could avoid questions of integrability, for example. But we can also define the entropy from the Kullback-Leibler divergence and write a specialized definition for the finite case that never asks about integrability if needed.