KL Divergence: Porting TLB into PFR

Stream: Polynomial Freiman-Ruzsa conjecture

[Pietro Monticone]

This topic is dedicated to the upcoming attempt to port KL divergence results from Testing Lower Bounds (TLB) into PFR in order to solve all B tasks.

[Yaël Dillies]

Sorry to rain on your parade, but have we really decided that making PFR depend on Rémy's project was not the way to go?

[Pietro Monticone]

I probably shouldn't have used the word "porting" in this case. What we meant was actually to make TLB a proper dependency for PFR. Sorry for the confusion.

[Yaël Dillies]

Ah okay sure. Then I think the first step is to complete #13740 so that we can bump PFR to a relatively recent Mathlib.

[Yaël Dillies]

I am trying to get #13740 off the ground, but I am graduating in two days, so no promise!