New PFR bounds, outstanding tasks V1

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

The third phase of the PFR project is now ready to begin. I have created a blueprint section to prove the PFR conjecture for general torsion, chopping it up into 46 definitions, lemmas, and theorems; see https://teorth.github.io/pfr/blueprint/sect0012.html . Later on Jyun-Jie Liao and I will also work to set up a similar blueprint for his refinement of the 2-torsion PFR exponent from 11 to 9.

Right now, only a small portion of the general torsion argument is ready to farm out to volunteers, but this should be enough to get started for now:

1. One-sided unconditional data processing inequality. This should be an easy application of existing entropy inequalities. Proven by Lorenzo Luccioli and Pietro Monticone
2. Unconditional data processing inequality This should follow quickly from two applications of #1. Proven by Lorenzo Luccioli and Pietro Monticone
3. Data processing inequality This should follow from #2 and a standard "Conditioning" argument that also appears already in many previous components of the PFR project. Completed by Paul Lezeau
4. Flipping a sign This is a Ruzsa distance inequality similar in nature to others already in PFR, such as the Ruzsa triangle inequality. It is moderately tricky, but should be doable. . Completed by Lorenzo Luccioli and Pietro Monticone
5. Kaimonovich–Vershik–Madiman inequality This should follow by induction from this previous inequality, but there may be an issue manipulating iIndepFun. Established by Lorenzo Luccioli and Pietro Monticone, conditional on #17
6. Kaimonovich–Vershik–Madiman inequality, II A corollary to #5 and other existing Ruzsa inequalities; again, the iIndepFun API may be the trickiest component. Claimed by Lorenzo Luccioli and Pietro Monticone, conditional on #17
7. Kaimonovich–Vershik–Madiman inequality, III Also follows from existing Ruzsa inequalities (though it does not directly use #5 or #6). Again, I anticipate iIndepFun API to be the most significant issue.
8. Sums of dilates, I Should be a straightforward application of existing Ruzsa distance inequalities. Completed by Lorenzo Luccioli and Pietro Monticone
9. Sums of dilates, II This should be a straightforward consequence of #8 and induction. Completed by Lorenzo Luccioli and Pietro Monticone
10. Comparing sums Should be a straightforward consequence of #6, existing entropy facts, and the finite sum API. Claimed by Paul Lezeau
11. Modify pfr#ProbabilityTheory.condIndep_copies so that the hypothesis [Fintype β] is relaxed to [FiniteRange Y]. This will allow many of the tools developed here to extend to infinite groups G. Completed by Lorenzo Luccioli and Pietro Monticone
12. Defining Multidistance Should be straightforward after invoking pfr#ProbabilityTheory.independent_copies'.
13. Multidistance of copy Should be routine once #12 is formalized.
14. Multidistance of independent variables Should be routine once #12 is formalized.
15. Nonnegativity Should follow quickly from pfr#max_entropy_le_entropy_add, once #12 is done.
16. Relabeling Should follow easily from Finset.sum API once #12 is done.
17. iIndepFun.finsets New API for independence that is needed for #5 and will likely also be useful elsewhere in the project.

That's maybe enough for now. I am envisioning a much more leisurely pace for this project than the three-week sprint we did for the m=2 case of PFR, but depending on how many volunteers we get, we may end up moving faster than I currently anticipate.

This thread has been rolled over to https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.202.2E0

[Yaël Dillies]

My exams end on the 11th of June. So expect the project to be done on the 12th :stuck_out_tongue_closed_eyes:

[Lorenzo Luccioli]

@Pietro Monticone and I opened a PR, proving mutual_comp_le. We had to add a few hypothesis to make the needed lemmas work.

[Pietro Monticone]

And PFR#190 proving mutual_comp_comp_le (2).

[Paul Lezeau]

Could I claim the task (3)?

[Pietro Monticone]

@Lorenzo Luccioli and I would like to claim task (4) if it's ok.

[Pietro Monticone]

Opened PFR#191 removing an unnecessary hypothesis from the two lemmas we proved in the previous PRs.

[Pietro Monticone]

We have just opened a draft including a first step of the proof of rdist_of_neg_le and the necessary lemma ProbabilityTheory.IdentDistrib.inv that should probably be ported to Mathlib (see our recent PR #12918).

We will work on these again in the next few days.

[Pietro Monticone]

We have opened a PR adding the proof of ent_of_sub_smul, which corresponds to the first part of task (8).

We claim the second part (i.e. ent_of_sub_smul').

[Pietro Monticone]

Opened a PR adding the proof of ent_of_sub_smul' (8.2).

[Pietro Monticone]

We have finished the proof of rdist_of_neg_le (task 4). Here is the associated PR which is finally ready for review.

[Terence Tao]

Wow, that was quite an amount of work - didn't anticipate that the manipulation of conditionally independent variables etc. would be so unwieldy! There are perhaps some minor golfing opportunities (e.g., I assume many of the by exact tactics can simply be deleted, and many of the measurability properties could presumably be resolved by measurability/fun_prop at the expense of increased heartbeats), but the important thing is that it is done.

[Pietro Monticone]

We tried to avoid using those by exacts, but the ones that we left throw errors (e.g. type mismatches). Anyone knows how to solve these? Here is an example.

We avoided the use of measurability in some places in order to make the proof significantly faster.

[Patrick Massot]

Did you try using a smiley?

[Patrick Massot]

I mean have mX'₁ : Measurable X'₁ := ((measurable_discrete fun x ↦ x.1).comp hXY'₁ :)

[Pietro Monticone]

Thank you very much, it works!

[Patrick Massot]

I know it looks super esoteric, I’m sorry.

[Pietro Monticone]

Opened PR golfing accordingly. Thanks again.

[Terence Tao]

Huh, that's a cute syntax. Is it asking Lean to cast the expression before the colon to the type that is being asked? But then why doesn't this happen automatically?

[Mario Carneiro]

The syntax (e :) means to elaborate e without expected type, and then assert that the result has whatever type it's supposed to be afterward. It's equivalent to by have := e; exact this, and it makes a difference sometimes because elaboration usually proceeds "backwards" treating the expected type as a goal and using that to fill variables, but sometimes you want to work "forwards" in term mode (just working out what you get with the inputs provided) and this is the term mode way to do it.

[Terence Tao]

I wonder how far off we are from having an AI copilot that can autocorrect nearly-working code such as have mX'₁ : Measurable X'₁ := (measurable_discrete fun x ↦ x.1).comp hXY'₁ into working code without having to know all these little tricks.

[Terence Tao]

Actually, I just tried Github Copilot. If you explicitly show it how to convert the first line, it will figure out the rest.

image.png

In fact, even without giving it the first line, it made the nearly-correct guess:

image.png

[llllvvuu]

re: measurability,

As someone who's often expanded measurability? due to speed, I found that fun_prop solved that issue for me and it is my first choice over measurability/continuity now. Since it's still early days for the fun_prop tactic, it occasionally needs to be helped along by turning on trace and adding @[fun_prop] to any lemma that it doesn't find (it can be done locally with attribute [fun_prop] the_lemma to avoid waiting on an upstream PR) or (disch := ...) for hairier things

[Pietro Monticone]

@Lorenzo Luccioli and I would like to claim task 9.

[Pietro Monticone]

We have finished the proof of ent_of_sub_smul_le (task 9) and opened the related PR.

[Pietro Monticone]

@Lorenzo Luccioli and I would like to claim task 11. Here you can find the related draft we are working on.

[Notification Bot]

A message was moved here from #Polynomial Freiman-Ruzsa conjecture > Mathlib bump by Pietro Monticone.

[Pietro Monticone]

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

In particular, we have:

• generalised condIndep_copies by relaxing the hypothesis [Fintype β] to [FiniteRange Y] (task 11)
• golfed the proof of condIndep_copies
• generalised identDistrib_of_sum
• added sum_meas_smul_cond_fiber' that generalises sum_meas_smul_cond_fiber by relaxing the hypothesis [DiscreteMeasurableSpace β] to [MeasurableSingletonClass β]

[Lorenzo Luccioli]

We also tried to generalize rdist_of_neg_le and ent_bsg, relaxing the Finset hypothesis to FiniteRange, but it’s not easy to do it, because during the proof we apply lemmas that require FiniteRange to the copies of our initial random variables, but being a copy of (i.e. identically distributed to) a function with finite range does not imply having finite range.
A way to solve this may be to modify the lemmas that produce the copies, so that they also output the hypotheses of FiniteRange for the copies.

However, these copies (at least in condIndep_copies) seem to be constructed as projections from the product of the codomains to each codomain, so in the case that the codomain is not finite this functions cannot hope to have a finite range. This means that the definition of the copies inside the proofs would have to be changed (maybe we could take the projections from the product of the ranges, and not the whole codomains), but I don’t know how hard it may be.

[Paul Lezeau]

Just opened a PR for task 3.

[Paul Lezeau]

Could I claim 10?

[Terence Tao]

Lorenzo Luccioli said:

We also tried to generalize rdist_of_neg_le and ent_bsg, relaxing the Finset hypothesis to FiniteRange, but it’s not easy to do it, because during the proof we apply lemmas that require FiniteRange to the copies of our initial random variables, but being a copy of (i.e. identically distributed to) a function with finite range does not imply having finite range.
A way to solve this may be to modify the lemmas that produce the copies, so that they also output the hypotheses of FiniteRange for the copies.

However, these copies (at least in condIndep_copies) seem to be constructed as projections from the product of the codomains to each codomain, so in the case that the codomain is not finite this functions cannot hope to have a finite range. This means that the definition of the copies inside the proofs would have to be changed (maybe we could take the projections from the product of the ranges, and not the whole codomains), but I don’t know how hard it may be.

Hmm. As Yael pointed out, the Mathlib version of all these tools may not use FiniteRange at all, so I guess it's not a priority to try to refactor these lemmas for now if there isn't a cheap way to do it. At any rate for the application to m-torsion PFR, we can safely assume that the ambient group is a Fintype, so there is no immediate need to extend these tools to the FiniteRange setting.

[Pietro Monticone]

@Lorenzo Luccioli and I would like to claim task 5. Here you can find the related draft we are working on.

[Pietro Monticone]

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

We added a few lemmas (see PR description), one of which is still to be proven (kernel.iIndepFun.finsets). The proof of kvm_ineq_I depends on it so it could be added as a new outstanding task.

[Pietro Monticone]

@Lorenzo Luccioli and I would like to claim task 6. Here you can find the related draft we are working on.