Outstanding tasks, version 2.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Time to roll over the outstanding tasks thread from the previous thread. One major new development is that the blueprint for the improved PFR constant C=9 in the 2-torsion case is now complete, so we can start formalizing that in parallel with the m-torsion tasks. Thanks to Jyun-Jie Liao for completing this blueprint!

Ongoing tasks:

• Kaimonovich–Vershik–Madiman inequality, II A corollary to Kaimonovich–Vershik–Madiman inequality and other existing Ruzsa inequalities; again, the iIndepFun API may be the trickiest component. Completed by Lorenzo Luccioli and Pietro Monticone
• Comparing sums Should be a straightforward consequence of Kaimonovich–Vershik–Madiman inequality, II, existing entropy facts, and the finite sum API. Claimed by Paul Lezeau

Outstanding tasks for the m-torsion project:
A.1. Kaimonovich–Vershik–Madiman inequality, III Follows from existing Ruzsa inequalities. I anticipate iIndepFun API to be the most significant issue. Completed by Lorenzo Luccioli and Pietro Monticone
A.2. Defining Multidistance Should be straightforward after invoking pfr#ProbabilityTheory.independent_copies'. Perhaps the definition of Ruzsa distance pfr#rdist can be a model? Completed by Terence Tao
A.3. Multidistance of copy Should be routine once item A.2 is formalized. Completed by Lorenzo Luccioli and Pietro Monticone
A.4. Multidistance of independent variables Should be routine once item A.2 is formalized. Claimed by Lorenzo Luccioli and Pietro Monticone
A.5. Nonnegativity Should follow quickly from pfr#max_entropy_le_entropy_add, once item A.2 is done.
A.6. Relabeling Should follow easily from Finset.sum API once item A.2 is done. Completed by Terence Tao
A.7. iIndepFun.finsets New API for independence that is needed for Kaimonovich–Vershik–Madiman inequality and will likely also be useful elsewhere in the project. Completed by Terence Tao
A.8 (Deleted due to being redundant)
A.9. Multidistance and Ruzsa distance I A relatively straightforward application of existing Ruzsa distance inequalities together with the definition of multidistance (A.2).
A.10. Multidistance and Ruzsa distance II A corollary of A.9 and existing Ruzsa distance inequalities.
A.11. Multidistance and Ruzsa distance III A more complicated application of Ruzsa distance inequalities.
A.12. Multidistance and Ruzsa distance IV Another more complicated application of Ruzsa distance inequalities.

Outstanding tasks for the 2-torsion project (mostly initially focusing on some basic API for Kullback-Leibler divergence):
B.1. Log sum inequality This should be a straightforward application of Jensen's inequality, though one may need to take care with edge cases involving division by zero. (May be redundant due to external projects involving KL divergence.)
B.2. Converse log sum inequality This should be a straightforward application of the converse to Jensen's inequality (already in Mathlib), though again the edge cases require care. (May be redundant due to external projects involving KL divergence.)
B.3. Kullback-Leibler divergence of copy Should be straightforward from definitions.
B.4. Gibbs inequality Should follow from B.1.
B.5. Converse Gibbs inequality Should follow from B.2.
B.6 Convexity of Kullback-Liebler A routine application of Jensen's inequality.
B.7. Kullback-Liebler and injections Should be routine from Finset.sum API.

We have chosen to achieve tasks B.3-B.7 (sidestepping the need for B.1, B.2) by first importing the relevant components of the "Testing Lower Bounds" project. Claimed by Lorenzo Luccioli and Pietro Monticone

Will keep adding to this list as progress continues. But one thing to highlight is that A.2 (definition of multidistance) will soon be a bottleneck to make further progress on the m-torsion project. Some thought may be needed to come up with a definition that makes the basic API (in particular A.3 and A.4) easy to establish.

[Lorenzo Luccioli]

About the KL divergence, it is already formalized in this repo (this is the file specifically about KL) where @Rémy Degenne and I are currently working.
It's written in a more general form than the one in the blueprint (in particular it's defined as the divergence between two measures), so it may need some work to be adapted to the finite case for random variables. But we already have some properties proven, like the Gibbs inequality.

[Terence Tao]

Hmm, this could potentially save some work, but I'm not sure how best to proceed since it seems your repo is also a work in progress. One possibility is to import selected definitions and results already obtained in your repo as black boxes with some sorries and derive the discrete cases we need from those boxes, and then try to remove the sorries at a much later date. Or we could adapt some of your code to the finite case. The arguments in the blueprint are pretty specific to the finite case I think, and would not benefit extensively from generalizing to arbitrary measures (for instance, I would imagine the converse Gibbs inequality would be significantly more subtle at that level of generality), so it is tempting for me to not try to aim for mathlib levels of generality here and just do something good enough for the current application. But I'd be interested to hear more thoughts.

[Lorenzo Luccioli]

I think that many of the results that would be needed are sorry-free, so even if the project is still in development, it should be safe to import them. The inverse Gibbs inequality is still not proven, but we plan on doing it in the near future.
As for the option to adapt our code to the finite case, this may require more work than the direct proof for the finite case, since many results about KL in our project rely on other lemmas about the more general f-divergences.

[Yaël Dillies]

Lorenzo, what's the horizon for integration in mathlib of your project? PFR already depends on APAP, so adding a second dependency is a recipe for mismatched Mathlib versions and other disasters (at least until the community on a single, uniform, versioning system)

[Yaël Dillies]

Lorenzo Luccioli said:

I think that many of the results that would be needed are sorry-free, so even if the project is still in development, it should be safe to import them.

I agree. The situation seems completely analogous to APAP which we already successfully depend upon.

[Rémy Degenne]

The horizon for integration in mathlib is not quite short term. We have PRed to mathlib several supporting lemmas about definitions that are already in mathlib and we will continue to do so as those come up, but for now we have not started PRing any new definition.

There were design decisions that were not clear at the beginning for some of the new definitions, so I wanted to wait and see how the definitions interacted before making any PR.
My intention is to merge most of the project to mathlib eventually, and we will make an effort towards that closer to the end of Lorenzo's internship (in September).

[Yaël Dillies]

I see three reasonable solutions then:

1. Sorry the results whose proofs will come from your repo
2. Keep the two repos in sync regarding the Mathlib version (seems like a pain since the repos are managed by a disjoint set of people)
3. Get APAP in Mathlib (at least the part relevant to proving BSG)

[Kim Morrison]

What would be helpful here in terms of version conventions, or support from lake?

[Kim Morrison]

Currently the only versions that Mathlib issues are tags for the first time Mathlib moves to each new Lean toolchain (e.g. v4.8.0 or v4.9.0-rc1)

[Kim Morrison]

There is no reason we couldn't also make regular tags, e.g. master-2024-06-12 each night, that might make it easier to communicate amongst project owners about which commit they would like to be on!

[Jyun-Jie Liao]

Actually I checked the proof again and I think the converse Gibbs is not needed in the end, so should be fine to remove it if that turns out to be the tricky part. Also in your project it seems that chain rule has been proved while convexity for f-divergence has not, so if we want to import what you already have, then Lemma 13.7 can be proved with chain rule + Gibbs instead, and then 13.5 (convexity) can also be removed. Then the only remaining place that would need Lemma 1.4 (log sum inequality) is Lemma 13.14, and Lemma 1.2 actually suffices in the proof of Lemma 13.14. So Lemma 1.4/1.5 can also be removed. This could potentially save some work. :stuck_out_tongue:

Lorenzo Luccioli said:

I think that many of the results that would be needed are sorry-free, so even if the project is still in development, it should be safe to import them. The inverse Gibbs inequality is still not proven, but we plan on doing it in the near future.
As for the option to adapt our code to the finite case, this may require more work than the direct proof for the finite case, since many results about KL in our project rely on other lemmas about the more general f-divergences.

[Rémy Degenne]

13.7 is also a special case of the data-processing inequality for KL, which we have.

[Rémy Degenne]

(but convexity of KL, which is the main argument in the blueprint proof of 13.7, is also a consequence of the data processing inequality, so no surprise here)

[Rémy Degenne]

1.4 seems to correspond to this lemma: https://remydegenne.github.io/testing-lower-bounds/blueprint/sect0003.html#lem:kl_ge

[Rémy Degenne]

To come back to the issue of depending on several projects: I have no experience with that so I don't know how much trouble the version mismatchs could be. I am updating mathlib in our project quite regularly so if @Yaël Dillies pings me whenever PFR needs to be updated i could update the project rather quickly.

There might be a better way to do this. As Kim writes, we could try coordinating on the mathlib versions that we use. It is not clear to me how to do that though: do I specify a version of mathlib by hand in my lakefile, and change the version by hand before calling lake update, like I have to change the lean-toolchain? Is there a way to tell lake that I only want to update if the mathlib version changed?

Anyway, I don't want to push the use of our project too much: the lemma we are talking about should not be too much trouble to prove again in the discrete case needed by PFR. It might just be simpler to do that.

[Terence Tao]

This is a great discussion! I just wanted to say that because this is a relatively low-risk project (the primary aims of PFR formalization have already been completed), this would be a good test case to implement any sort of experimental workflow (e.g., working with multiple pre-mathlib imports) in order to learn any lessons that could be useful for future projects (e.g., one could imagine the FLT project facing a comparable issue at some point). So while we could go for a minimalistic route here of reducing the exposure of PFR to the theory of KL divergence as much as possible to avoid this particular issue, we could also use the opportunity to do a test in a situation where "failure" is not too painful (we always have the option of commenting out any integration attempts at a later date, and instead proving the small number of KL divergence lemmas that we need "by hand" in the finite case). But taking the path of least resistance and just proving the lemmas by hand from the start is also OK with me.

But perhaps at a bare minimum we can try to synchronize the notation and spelling with the project. I am certainly not attached to the current spelling KL[X ; μ # Y ; μ'] for KL divergence that I hastily implemented as a cut and paste from similar notation from previous parts of PFR - am open to suggestions to make notation that is more compatible both with the lower bounds project and with general mathlib conventions.

[Yaël Dillies]

Terence Tao said:

because this is a relatively low-risk project (the primary aims of PFR formalization have already been completed), this would be a good test case to implement any sort of experimental workflow

I agree! Let's figure this out.

[Yaël Dillies]

Rémy Degenne said:

I am updating mathlib in our project quite regularly so if @Yaël Dillies pings me whenever PFR needs to be updated i could update the project rather quickly.

New mathlib versions are so frequent that even if I ping you right as I update there's a very high chance that you wil need to specify the mathlib version by hand...

Kim Morrison said:

What would be helpful here in terms of version conventions, or support from lake?

Currently the only versions that Mathlib issues are tags for the first time Mathlib moves to each new Lean toolchain (e.g. v4.8.0 or v4.9.0-rc1)

There is no reason we couldn't also make regular tags, e.g. master-2024-06-12 each night, that might make it easier to communicate amongst project owners about which commit they would like to be on!

... hence I agree that it would help a huge lot to have daily named commits for mathlib, and on top of that a simple way to tell lake update that we want to use such commits.

[Yaël Dillies]

@Kim Morrison, is something like this reasonable expectations?

• Have a bot automatically create version branches. Here "version" could mean either Lean toolchains or named mathlib commits. Not sure which one is best.
• Have a --dep flag to lake update to specify which dependency we want to update. When lake update --dep preferred_dep is run, the lake-manifest inherits the versions of all dependencies of preferred_dep, and all dependencies of the project that are not dependencies of preferred_dep are updated to the latest version of mathlib that's earlier than preferred_dep's.

[Yaël Dillies]

Hmm, looks a bit complicated :thinking:

[Kim Morrison]

You know that you can already write lake update dep to update just one of your dependencies?

[Kim Morrison]

I'll arrange for master-YYYY-MM-DD tags on Mathlib.

[Yaël Dillies]

Kim Morrison said:

You know that you can already write lake update dep to update just one of your dependencies?

That's not exactly what I want, right? I want to update that one dependency and also the dependencies of that dependency

[Kim Morrison]

I think if you don't specify transitive dependencies in your lakefile, then this is the behaviour you get already, no?

[Lorenzo Luccioli]

Update: now we have the converse Gibbs' inequality for the general kl divergence. See this PR.

[Terence Tao]

That's great! In view of the discussion I then propose trying to import enough of the lower bounds project to establish B.3-B.5 (B.1 and B.2 were only introduced to establish B.4 and B.5 respectively, so if you already have Gibbs and converse Gibbs in your repo, we don't need to establish this separately). This is overkill for the PFR project, but it would be good to get some practice in how one project can "cite" another, as this is obviously something that will keep happening in the future (as it would be unrealistic to demand that every possible citeable mathematical fact be placed in mathlib).

[Pietro Monticone]

We have just completed task 6 and opened the related PR.

NB: We added an auxiliary lemma (see PR description).

[Pietro Monticone]

@Lorenzo Luccioli and I would like to claim task A.1.

[Terence Tao]

I've made the following first stab at A.2 (defining multidistance), which at least passes the Lean compiler, but I am not sure if this version is at all aligned with good Lean practices. Firstly it might be possible to have the entropy functional H[] automatically detect the volume measure from the MeasureSpace structure. I'm also not committed to using Fin m as the indexing set; that's how we use it in the blueprint, but it might be marginally better to work either with an arbitrary Fintype or with a Finset of an arbitrary type. One could also use the measure-based version Hm[] of entropy instead of the random variable-based version (this is how Ruzsa distance is defined). I guess the precise definition might not be super important as long as core API such as A.3-A.6 are easy to prove. Anyway, any thoughts would be appreciated.

/--  Let `X_[m] = (X₁, ..., Xₘ)` be a non-empty finite tuple of `G`-valued random variables `X_i`.
Then we define `D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i']`, where the `X_i'` are independent copies
of the `X_i`.-/
noncomputable
def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i))
  (X : (i : Fin m) → (Ω i) → G) : ℝ := H[ fun ω ↦ ∑ i, (X i) (ω i); .pi (fun i ↦ (hΩ i).volume)] - (m:ℝ)⁻¹ * ∑ i, H[X i; (hΩ i).volume]

[Pietro Monticone]

We have just completed task A.1 and opened the related PR.

NB: We added an auxiliary lemma and we slightly changed the original statement (see PR description).

[Terence Tao]

Pietro Monticone said:

We have just completed task A.1 and opened the related PR.

NB: We added an auxiliary lemma and we slightly changed the original statement (see PR description).

Wow, that was fast! Sounds like you have figured out how to handle all the iIndepFun issues. I realized that there was one final application of the Kaimonovich-Vershik-Madiman inequalities that is in a similar spirit that I had neglected to put on the "outstanding tasks" list, so I added it just now as A.7.

[Terence Tao]

Terence Tao said:

I've made the following first stab at A.2 (defining multidistance)

Since there wasn't any objection, I've gone ahead and approved this definition (I did discover that I could at least drop the final (hΩ i).volume as autoparam was able to figure this out already), and formalized the statement of several more lemmas that use multidistance.

[Pietro Monticone]

Is task A.8 the same one claimed by @Paul Lezeau?

If not, @Lorenzo Luccioli and I would like to claim A.8.

[Terence Tao]

Oops, that is a duplicate, sorry! Removing it now.

[Pietro Monticone]

@Lorenzo Luccioli and I would like to attempt the porting of the KL divergence from the Testing Lower Bounds project in order to solve the B.X tasks.

We have just opened the related topic.

[Pietro Monticone]

We would like to claim task A.3.

[Terence Tao]

Great! Feel free to modify the definition of multidistance if it makes basic API like A.3 and A.4 easier to establish.

[Pietro Monticone]

We have just completed task A.3 and opened the related PR.

We slightly modified multiDist along the same lines of rdist as follows:

def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i))
     (X : (i : Fin m) → (Ω i) → G) : ℝ :=
   H[fun x ↦ ∑ i, x i; .pi (fun i ↦ (hΩ i).volume.map (X i))] - (m:ℝ)⁻¹ * ∑ i, H[X i]

[Pietro Monticone]

We would like to claim task A.4 too. Here is the associated draft PR we're working on.

[Terence Tao]

Just a note that this project is not completely dead! I have recently started filling in a variety of tasks, including A.6 and some later results not currently listed on the "outstanding task list", in particular the very final result pfr#pfr-torsion is now locally proven (of course its main dependency, pfr#pfr_aux_torsion, remains incomplete). I plan to work on A.7 next.

[Sébastien Gouëzel]

I am currently bumping the project to latest mathlib. Not a trivial task because of the new variable mechanism, but I think it's worth it to make sure we can PR some parts to mathlib later on.

[Paul Lezeau]

I'm still planning on completing the "Comparing sums" lemma (I've been distracted by various PhD related tasks and projects lately, but should hopefully have more time in the upcoming weeks!)

[Yaël Dillies]

Sébastien Gouëzel said:

I am currently bumping the project to latest mathlib. Not a trivial task because of the new variable mechanism, but I think it's worth it to make sure we can PR some parts to mathlib later on.

Sébastien, we had someone who wanted to use PFR on 4.9 for some AI training. Would it be possible for you to first bump to 4.9 then to 4.11.0-rc2 ?

[Sébastien Gouëzel]

Sorry, I went straight for 4.11...

[Terence Tao]

A.7 now done. (Maybe with a bit more wrestling in the mud with dependent types than strictly necessary, but still managed to reach the finish line.)

[Terence Tao]

Just a notification that I have merged @Sébastien Gouëzel 's bump to 4.11. It took a few minutes to recompile Lean, lake, and PFR, and I had to restart a few times, but it was generally without problems. Just to quote from Sebastien's PR:

Warning: since it changes the Lean and mathlib version, you will need to redownload the cache once you have merged this one, by doing lake exe cache get (and if this one fails, then erase your .lake folder and do lake exe cache get again).

[Terence Tao]

I don't know if this is a consequence of the bump, or of the code I am writing, but the lean compiler (on VSCode on a Windows machine) has become unstable for me, at least when working of MoreRuzsaDist.lean; it runs for maybe five minutes and then crashes. Not sure what the problem is...

[Error - 6:46:13 PM] Request textDocument/completion failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/codeAction failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/documentSymbol failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/codeAction failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/codeAction failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/codeAction failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/documentHighlight failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/documentHighlight failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902

[Error - 6:46:13 PM] Request textDocument/documentHighlight failed.

Message: Server process for file:///c%3A/Users/teort/Dropbox/Lean/pfr/PFR/MoreRuzsaDist.lean crashed, likely due to a stack overflow or a bug.

Code: -32902```

[Yaël Dillies]

Yes, I get a lot of these too... I thought it might be caused by the haveLet linter, but I am not sure anymore

[Kim Morrison]

Oh, I just managed to reproduce a crash in this file, and got the following stack trace:

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system) interpreter stacktrace: #1
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #2
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #3
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #4
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #5
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #6
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #7
Mathlib.Linter.haveLet.InfoTree.foldInfoM._at.Mathlib.Linter.haveLet.nonPropHaves._spec_15._lambda_1 #8
Mathlib.Linter.haveLet.InfoTree.foldIn...

[Kim Morrison]

So it is the haveLet linter.

[Kim Morrison]

Hopefully for now set_option linter.haveLet 0 will suffice

[Kim Morrison]

@Damiano Testa is thinking about reimplementing that linter, so hopefully the bug is short-lived.

[Kim Morrison]

It might be a good idea to just disable it in the PFR lakefile for now.

[Kim Morrison]

Or, given how many problems this is causing, just disable it entirely in Mathlib until there is a reimplementation...

[Yaël Dillies]

Yes, it has already caused me to comment out huge chunks of proofs

[Damiano Testa]

I am indeed trying to fix these issues, but I have a busy week ahead of me: I'll just make a PR to disable the linter on mathlib for the moment.

[Kim Morrison]

Thank you. :-)

[Damiano Testa]

#16058

[Sébastien Gouëzel]

Mathlib bump with the above fix included at https://github.com/teorth/pfr/pull/223

[Terence Tao]

This seems to have fixed the problem. Also, subjectively, compilation of the Lean code appears to be slightly faster, which is a nice bonus.

[Sébastien Gouëzel]

It's not clear to me how much the project is alive. Still, I'd like to get to the exponent 9 instead of 11, so I started hacking a little bit on KL divergence. PR at PFR#227. As I say in the PR, to get correct statements, I had to assume that the KL divergence was finite, i.e., that X is absolutely continuous wrt Y. It's not clear to me yet if it's better to work having this condition around, or to have a version of KL divergence taking values in extended nonnegative reals. I'll see as things go...

[Yaël Dillies]

Sébastien Gouëzel said:

It's not clear to me how much the project is alive

Progress on the mathematics seems to have mostly stalled. Progress on upstreaming has never been so fast. cf the PRs from PFR

[Sébastien Gouëzel]

Yes, I've definitely noticed the PRs. Many thanks for that!

[Terence Tao]

Thanks for all the work! I’be been distracted by other projects but will set up a fresh thread here soon to try to maintain the fresh momentum.