Outstanding tasks, version 4.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Time for another rollover of the "outstanding tasks" thread! Nearing the finish line! The previous thread can be found here.

It's somewhat moot now that the project is nearing its end, but I have expanded on the format of this "outstanding task list" to also include documentation tasks and administrative tasks. I would imagine that for a larger project, all three sets of tasks would be completed somewhat in parallel (with the administrative tasks covering a somewhat larger region of the project space than the documentatation tasks, which in turn should be covering a larger region than the formalization tasks, so that all three regions can expand concurrently), and be handled by three somewhat independent groups of contributors.

Existing claims:

1. @Jonas Bayer, @llllvvuu , and @Paul Lezeau have established Bounded entropy implies concentration.
2. @Yaël Dillies and @Bhavik Mehta claim Entropic Balog-Szemeredi-Gowers
3. @Rémy Degenne has established Alternate form of distance
4. @Paul Lezeau has established Entropy of uniform random variable
5. @Sebastien Gouezel has established Polynomial Freiman-Ruzsa conjecture
6. @Ben Eltschig has established Second estimate
7. @Arend Mellendijk has established tau decrement

Outstanding formalization tasks:

1. Symmetry identity This should follow from Copy preserves entropy and definitions; some partial progress had already been made on this by @Kyle Miller, but more remains to be done. Established by @Mantas Baksys
2. Bound on distance increments This should be a straightforward linear combination of Entropy bound on quadruple sum and Comparison of Ruzsa distances, II Claimed by @Paul Lezeau and @Jonas Bayer
3. Constructing good variables. I This is a moderately complicated linear combination of previous inequalities. Established by @Floris van Doorn
4. PFR in infinite groups A (hopefully) quick corollary of PFR in the case of infinite groups. Established by @Patrick Massot

Outstanding documentation/blueprint/examples tasks:

1. Writing examples to illustrate probability kernels.
2. Writing examples to illustrate Shannon entropy.
3. Writing examples to illustrate Ruzsa distance.
4. Writing examples to illustrate the finiteness tactic.
5. Writing examples to illustrate real-valued measures.

Outstanding administrative tasks:

1. Scour the code for outstanding sorries and any other issues that warrant placing in this list. Established by @Terence Tao
2. Add blueprint specification for an extension of PFR to infinite elementary abelian 2-groups. Established by @Terence Tao

[Sebastien Gouezel]

https://github.com/teorth/pfr/pull/96 removes all sorries in the file main.lean proving the final conjecture.

[Paul Lezeau]

@Jonas Bayer and I would like to claim 2 if no one has made a start on that

[Mantas Baksys]

I would like to claim 1 in case no one else has started work on it

[Floris van Doorn]

I can work on 3, if that is the last unclaimed tasks left...

[Terence Tao]

Floris van Doorn said:

I can work on 3, if that is the last unclaimed tasks left...

Great! I've taken the liberty of writing up a provisional formal statement of Entropic Balog-Szemeredi-Gowers which is one of the key inputs in the proof. Hopefully @Yaël Dillies or @Bhavik Mehta can chime in on whether this statement aligns with what they think they could prove (but if there are only minor differences then it should not be too difficult to reconcile afterwards).

This one might be slightly more tricky than the other "take linear combinations of existing inequality" type arguments, so please let us know if you need assistance (e.g., if you find a sublemma that you need but can't prove, you can spin it off with a sorry to put back on the outstanding task list).

[Floris van Doorn]

Great! I was indeed still puzzling on how to write that. I think I'll replace the LHS by
(μ.map Z)[fun z ↦ d[ A; μ[|Z⁻¹' {z}] # B ; μ[|Z⁻¹' {z}] ]] (using the same notation as I saw in condEntropy).

[Ben Eltschig]

Terence Tao said:

Floris van Doorn said:

I can work on 3, if that is the last unclaimed tasks left...

Great! I've taken the liberty of writing up a provisional formal statement of Entropic Balog-Szemeredi-Gowers which is one of the key inputs in the proof. Hopefully Yaël Dillies or Bhavik Mehta can chime in on whether this statement aligns with what they think they could prove (but if there are only minor differences then it should not be too difficult to reconcile afterwards).

This one might be slightly more tricky than the other "take linear combinations of existing inequality" type arguments, so please let us know if you need assistance (e.g., if you find a sublemma that you need but can't prove, you can spin it off with a sorry to put back on the outstanding task list).

Speaking of troublesome sublemmas, I think I may have one of those in the second estimate already :sweat_smile:

If I'm seeing things right the proof in the blueprint requires d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] ≤ d[X₁ + X₁' # X₂ + X₂'] in order to obtain the inequality (2), but I've had no luck proving it so far - is that even right, or am I on the wrong track? If it is, is there an easy proof of this or should I just leave it as a sorry for now?

[Ben Eltschig]

Other than that the proof is pretty much done by the way, I'm just still in the process of filling in a few technical sorries related to independence. Hopefully I'll be able to PR it later today or tomorrow.

[Terence Tao]

Ben Eltschig said:

Speaking of troublesome sublemmas, I think I may have one of those in the second estimate already :sweat_smile:

If I'm seeing things right the proof in the blueprint requires d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] ≤ d[X₁ + X₁' # X₂ + X₂'] in order to obtain the inequality (2), but I've had no luck proving it so far - is that even right, or am I on the wrong track? If it is, is there an easy proof of this or should I just leave it as a sorry for now?

That's weird, you should only need a lower bound on d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] and not an upper bound (certainly not this one). Could you elaborate a bit more on where that bound is coming up? The bound (2) in the blueprint should be a linear combination of the four preceding inequalities as well as Lemma 6.14.

[Ben Eltschig]

The lower bound on d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] comes from Lemma 6.7 as you said in the blueprint, but since the rewritten Lemma 5.2 involves d[X₁ + X₁' # X₂ + X₂'] too I need a lower bound on that as well. That's what I used the d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] ≤ d[X₁ + X₁' # X₂ + X₂'] for, to make sure the lower bound from Lemma 6.7 holds for both. Or should some other lower bound be used instead?

[Terence Tao]

Ben Eltschig said:

The lower bound on d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] comes from Lemma 6.7 as you said in the blueprint, but since the rewritten Lemma 5.2 involves d[X₁ + X₁' # X₂ + X₂'] too I need a lower bound on that as well. That's what I used the d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] ≤ d[X₁ + X₁' # X₂ + X₂'] for, to make sure the lower bound from Lemma 6.7 holds for both. Or should some other lower bound be used instead?

Lemma 6.14 should be used to get the lower bound for d[X₁ + X₁' # X₂ + X₂'].

[Ben Eltschig]

oh, I see :sweat_smile:
sorry about that then, looks like I've been overthinking it

[Patrick Massot]

Do I understand correctly that there is no remaining unclaimed lemma? I wanted to try to prove at least one lemma, but I was on family duty during the Thanksgiving break so I may have missed the opportunity.

[Terence Tao]

Patrick Massot said:

Do I understand correctly that there is no remaining unclaimed lemma? I wanted to try to prove at least one lemma, but I was on family duty during the Thanksgiving break so I may have missed the opportunity.

Ha, yes the project has proceeded faster than expected and all the main tasks have already been claimed. But there was one auxiliary lemma that would be appreciated I think. Right now, the main theorem requires the ambient group G (which is what in the blueprint is called ${\mathbb F}_2^n$ to be a finite elementary abelian 2-group. However, it should be possible to remove the finiteness hypothesis on G (but then one has to place finiteness hypotheses on H, A, c as a consequence). The point is that any finite subset A of an infinite elementary abelian 2-group will generate a finite subgroup and one can work in there. So if you want to contribute, one possibility is to state and prove such a generalization as a corollary of the main theorem. This isn't explicitly listed as a goal in the blueprint or in the outstanding tasks, but I can add the precise specifications for it in a few hours if you would like to claim it (but perhaps you see already what the generalization should be and how to prove it).

[Patrick Massot]

Ok, I will work on that.

[Kalle Kytölä]

I was just removing one ad hoc lemma I had introduced earlier, by providing an instance of ElementaryAddCommGroup for functions (random variables) with values in an ElementaryAddCommGroup.

I made a PR, which contains a few small lemmas for this purpose. These might or might not be useful for what @Patrick Massot is doing now, although Patrick probably proves them quicker and more elegantly that I did anyway.

[Ben Eltschig]

The second estimate should be done too now with #102. There's still a few things to clean up, but I probably won't get to those before tomorrow.

[Terence Tao]

Patrick Massot said:

Ok, I will work on that.

I've just uploaded a stub of a statement (see PFR_conjecture' in main.lean) and the blueprint should also update in a few minutes as well.

[Patrick Massot]

I think your statement is not what you intended because your assumptions do not imply A is finite. The trap is that Nat.card is defined to be zero for infinite types.

[Patrick Massot]

But that's not a problem, I already wrote a statement.

[Terence Tao]

In reviewing all the Lean files, I came across FiniteMeasureFintype.lean, which does not seem to be linked to from any other file in the project, and still contains some sorries. Is someone still working on this file, and is there a plan to integrate it into the project and/or to move some or all of it to the Mathlib folder? Similarly for ProbabilityMeasureProdCont.lean, although here there are no outstanding sorries.

[Floris van Doorn]

Kalle Kytölä said:

I was just removing one ad hoc lemma I had introduced earlier, by providing an instance of ElementaryAddCommGroup for functions (random variables) with values in an ElementaryAddCommGroup.

Oh good! I also realized I needed that to simplify some arguments a bit.

[Dustin Mixon]

In the blueprint, the hypothesis of "PFR in infinite groups" includes "A \subset A", but I bet this should be "A \subset G".

[Sebastien Gouezel]

Terence Tao said:

In reviewing all the Lean files, I came across FiniteMeasureFintype.lean, which does not seem to be linked to from any other file in the project, and still contains some sorries. Is someone still working on this file, and is there a plan to integrate it into the project and/or to move some or all of it to the Mathlib folder? Similarly for ProbabilityMeasureProdCont.lean, although here there are no outstanding sorries.

I think you can just remove FiniteMeasureFintype.lean. On the other hand, ProbabilityMeasureProdCont.lean is needed to show that the Rusza distance is continuous as a function of two probability measures (which is useful to show the existence of a tau-minimizer).

[Patrick Massot]

I finished deducing the infinite version from the finite one. PR is at https://github.com/teorth/pfr/pull/109.

[Johan Commelin]

Only two non-green vertices left in https://teorth.github.io/pfr/blueprint/dep_graph_document.html !

[Floris van Doorn]

There are still 3 sorries (outside comments, outside the Test folder). The third is rdist_triangle which is marked in the tex file as \leanok, but still is proven by sorry.

[Rémy Degenne]

The version we need for the project is ok. This sorry is for the kernel rdist and is not needed.

[Rémy Degenne]

I thought we needed the triangle inequality for cond_rdist, so I started working on the kernel version to then specialize it to the conditional kernel, but the conditional version is in fact not needed for the project.

I'm still trying to prove the kernel rdist_triangle even though it's not needed. I have a partial proof here: https://github.com/RemyDegenne/pfr/blob/master/PFR/Entropy/KernelRuzsa.lean#L222 . However I am running into issues like proving that the entropy of a Markov kernel from S × T with a product measure to some other space is the same as the entropy of the same kernel seen as a kernel from S × S' × T (where we also augment the measure with an arbitrary measure on S'). There is nothing mathematically difficult there, but the kernel manipulations are tedious.

This project revealed some friction in the use of Markov kernels. I added several simp lemmas and PRed some to Mathlib, but it's not yet satisfactory. Several ruzsa_triangle_aux lemmas in the same file are also there only because I have trouble proving that some kernels are equal. Like this one:

lemma ruzsa_triangle_aux1 (κ : kernel T (G × G)) (η : kernel T G)
    [IsMarkovKernel κ] [IsMarkovKernel η] :
    map (κ ×ₖ η) (fun x ↦ x.1.1 - x.1.2) (measurable_of_finite _)
      = map κ (fun p ↦ p.1 - p.2) measurable_sub :=

The current proof is 13 lines (which could surely be golfed to slightly less), but ideally it should be much shorter.

[Rémy Degenne]

Well, I just found a two-lines proof. Perhaps the issue was simply that I was tired when writing those :)

lemma ruzsa_triangle_aux1 (κ : kernel T (G × G)) (η : kernel T G)
    [IsMarkovKernel κ] [IsMarkovKernel η] :
    map (κ ×ₖ η) (fun x ↦ x.1.1 - x.1.2) (measurable_of_finite _)
      = map κ (fun p ↦ p.1 - p.2) measurable_sub := by
  have : (fun x : (G × G) × G ↦ x.1.1 - x.1.2) = (fun x ↦ x.1 - x.2) ∘ Prod.fst := by ext1 y; simp
  rw [this, ← map_map, ← kernel.fst, fst_prod]

But the general remark about kernel manipulation is still true: they are not as easy to use as they should be.

[Terence Tao]

Given that we may temporarily have a surplus of volunteers for the PFR project as it nears completion, I thought of one additional small task that someone might be willing to work on. Right now our main theorem is stated for elementary abelian 2-groups, but in the literature the PFR is stated instead in terms of vector spaces over F_2. So having a small lemma that says that vector spaces over F_2 are always elementary abelian 2-groups would be nice. There was previous talk in this thread about having a lean file with some showcase results from the project (similar to this file for a Ramsey theory project), and being able to state the PFR for vector spaces over F_2 (with the proof outsourced to the other lean files, of course) would be a natural candidate for such a file.

[Scott Morrison]

https://github.com/teorth/pfr/pull/114

[Terence Tao]

Scott Morrison said:

https://github.com/teorth/pfr/pull/114

Wow, that was quick! Thanks!

[Scott Morrison]

It did usefully uncover some missing functionality in exact?. This was my pre-golfed version:

def ofModule [AddCommGroup G] [Module (ZMod p) G] [Fact p.Prime] : ElementaryAddCommGroup G p where
  orderOf_of_ne := @fun x h => by
    suffices p • x = 0 by hint
    -- Sadly, this didn't work, but should have?
    -- have : Basis _ (ZMod p) G := by exact?
    have b : Basis _ (ZMod p) G := .ofVectorSpace (ZMod p) G
    -- Finding `Basis.ext_elem` was most of the work: what search tool could have helped?
    apply Basis.ext_elem b
    hint

The problem with using exact? to find the basis was that I knew that I had to leave the indexing type blank, because I wouldn't know that until I found the relevant function. However exact? appears to be unwilling to unify that blank.

[Eric Rodriguez]

I'm not sure how similar this is to LTE in this sense, but I wonder if there is some definitions that could have some explicit theorems listed out and collected in a file to show that the definitions are correct?

[Eric Rodriguez]

Something like https://github.com/leanprover-community/lean-liquid/blob/master/src/examples/Ext.lean

[Terence Tao]

Eric Rodriguez said:

I'm not sure how similar this is to LTE in this sense, but I wonder if there is some definitions that could have some explicit theorems listed out and collected in a file to show that the definitions are correct?

I like this idea! I have just created an examples file on the github repository in which we could put examples to illustrate various results and methods established as a consequence of the PFR project. Right now the only code it contains is a self-contained statement of the PFR conjecture (phrased using modules instead of elementary abelian groups), but it contains empty sections to illustrate probability kernels, Shannon entropy, Ruzsa distance, the finiteness tactic, and real-valued measures. I have therefore added to the outstanding task list the task of writing up some examples for each of these sections, in case there are volunteers to do so. Feel free to also propose other sections to showcase other byproducts of the project!

[Floris van Doorn]

I think for LTE the examples folder was mostly there to show that the statement of the main theorem was correct, by showing that the definitions used in it have the properties that one would expect. Lean checks that the definitions used in the proof (but that do not occur in the statement) are "correct" in the sense that they suffice to prove the final statement.
In this project, the final statement is very elementary.

[Thomas Bloom]

It would be nice to also have the equivalent formulation of PFR in terms of approximate homomorphisms (see e.g. Proposition 10.2(4) of Ben Green's notes https://arxiv.org/abs/math/0409420), this is often the form in which it is applied in computer science for example.

[Terence Tao]

Floris van Doorn said:

I think for LTE the examples folder was mostly there to show that the statement of the main theorem was correct, by showing that the definitions used in it have the properties that one would expect. Lean checks that the definitions used in the proof (but that do not occur in the statement) are "correct" in the sense that they suffice to prove the final statement.
In this project, the final statement is very elementary.

Right, the only custom definition we actually used to state PFR was ElementaryAddCommGroup, but now that we have that every instance of Module (ZMod 2) is also an instance of ElementaryAddCommGroup 2, it was easy to write a completely self-contained version of PFR, which I did in the examples file. But in addition to PFR we did also develop a lot of tools regarding Shannon entropy, Ruzsa distance, etc. that could potentially be useful for other projects as well, and I thought that the examples file could be used to illustrate that the definitions we have for say d[ X # Y ] or I[ X : Y | Z] do in fact agree with the standard definitions, using only the standard Mathlib functions to state the equivalence. In many cases this just amounts to restating some of the helper lemmas that we already have in the code, but those lemmas are buried amongst dozens of other lemmas and might not be easily discernable to the casual reader.

@Thomas Bloom : Good idea. If I have time in the next day or two I may try to write up a blueprint of how to derive the approximate homomorphism version of PFR from the combinatorial version. (I'm glad you didn't request 10.2(5) though, as that requires the combinatorial Balog-Szemeredi-Gowers lemma which we don't have formalized yet.)

EDIT: in order to take advantage of the great volunteer community we have here, I have gone ahead and quickly written up a blueprint which should appear shortly at https://teorth.github.io/pfr/blueprint/sect0008.html (or at https://github.com/teorth/pfr/blob/master/blueprint/src/chapter/homomorphism.tex if you are too impatient to wait for the blueprint to compile), and started a new thread to announce the new tasks.

[Adam Topaz]

Yes, what Eric and Floris said is correct: the examples folder in LTE is there to illustrate that the definitions are correct. But it may still be worthwhile to do this for PFR for similar reasons, even if the definitions are more elementary.

[Adam Topaz]

For example, the statement

theorem PFR_conjecture' {G : Type*} [AddCommGroup G] [ElementaryAddCommGroup G 2]
    {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite)
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : AddSubgroup G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < 2 * K ^ 12 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by

involves a "nonstandard" (meaning not in mathlib) definition ElementaryAddCommGroup which could be (easily) described with some nice exampels (e.g. showing that an additive group satisfies this if and only if the $\mathbb{Z}$-module structure "descends" to a $\mathbb{Z}/2$-module structure).

[Yaël Dillies]

Re combinatorial BSG: Bhavik and I are also working on that