feat: Improve other bounds using PFR 9 #232
Conversation
| norm_cast | ||
|
|
||
| #print axioms better_PFR_conjecture | ||
|
|
There was a problem hiding this comment.
By the way, this examples file is very much broken. I guess it isn't tested by CI, and I'm not sure what its role is.
There was a problem hiding this comment.
I think it is referenced on Terry's blog? It should very much be checked by CI!
|
Yeah, it's supposed to allow someone with basic understanding of Lean, but not of the various technical definitions used in the PFR project, to be able to be convinced of the final results of the project. But it hasn't been maintained in months and so is indeed a bit broken. Were you able to get it to run with the latest build? If so we can try to explicitly import it in the master Lean file so that it is covered by CI going forward. |
We will need to move it into the |
|
Sure, will do. If you are willing to do the move as a PR I will update links accordingly. |
|
Here is the PR: #233 |
Improve the homomorphism version and approximate homomorphism version of PFR. It's not obvious if PFR 9 also gives an improvement for weak PFR over Z^d as the proof really uses the entropic control, which is not provided by the Kullback-Leibler divergence argument, so I haven't done anything there.