Outstanding tasks for PFR III, version 4.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

This is as good a time as any to update the "outstanding tasks" thread. (If this project were not so close to completion, it might be worth switching over to a Github issues project management system, but this older method should still suffice for now.)

Thanks to the heroic efforts of @Sébastien Gouëzel, one of the primary goals of PFR III - to get the constant C down from 11 to 9 - is now completed! The remaining primary goal - the extension to m-torsion groups - is about halfway done, with 18 sorries remaining. In addition, we now have a small side project to upgrade "affine" to "linear" in the approximate homomorphism form of PFR.

The already claimed tasks are:
Ongoing tasks:

• Comparing sums Should be a straightforward consequence of Kaimonovich–Vershik–Madiman inequality, II, existing entropy facts, and the finite sum API. Completed by @Paul Lezeau

Outstanding tasks for the m-torsion project:
A.1.  Multidistance and Ruzsa distance I A relatively straightforward application of existing Ruzsa distance inequalities together with the definition of multidistance. Completed by @Terence Tao
A.2. Multidistance and Ruzsa distance II A corollary of A.1 and existing Ruzsa distance inequalities. Completed by @Terence Tao
A.3. Multidistance and Ruzsa distance III A more complicated application of Ruzsa distance inequalities. Completed by @Terence Tao
A.4. Multidistance and Ruzsa distance IV Another more complicated application of Ruzsa distance inequalities. Completed by @Terence Tao
A.5. Existence of minimizer This is in theory just a modification of pfr#tau_minimizer_exists, but there could be potential subtleties. Completed by @Sébastien Gouëzel
A.6. Multidistance chain rule corollary In principle this is just telescoping pfr#iter_multiDist_chainRule, but there may be subtleties particularly regarding independence. Completed by @Terence Tao
A.7. Bounding mutual information Applies the previous corollary and a bunch of previous entropy estimates. Claimed by @Terence Tao
A.8. Multidistance of independent variables  This should follow from the definition of multidistance and the existing API for entropy of independent random variables (but possibly there are technical issues regarding how Lean treats joint independence). Completed by @Terence Tao
A.9 Entropy of W Should be a routine application of existing entropy estimates. Completed by @Terence Tao
A.10 Application of BSG The analogue of https://teorth.github.io/pfr/blueprint/sect0006.html#construct-good-prelim. Should be a routine application of entropy estimates including the entropic BSG lemma. Completed by @Terence Tao
A.11 Entropy of Z_2 Should be a routine application of existing entropy estimates. Completed by @Terence Tao
A.12 Mutual information bound I A moderately complex application of A.7. Completed by @Terence Tao
A.13 Mutual information bound II Should be a routine application of existing entropy estimates. Completed by @Terence Tao
A.14 Distance bound Should be a routine application of existing entropy estimates and the previous lemmas. Completed by @Terence Tao
A.15 Vanishing entropy Moderately long algebraic calculation using many previous lemmas. Completed by @Terence Tao
A.16 Entropy form of PFR This is similar to https://teorth.github.io/pfr/blueprint/sect0006.html#entropy-pfr and should be straightforward. Completed by @Terence Tao
A.17 PFR This is similar to https://teorth.github.io/pfr/blueprint/sect0007.html#pfr_aux and should be straightforward. Completed by @Terence Tao

And the new project:
B.1. Duality of finite abelian 2-groups There should be some API in Mathlib to help out with this one, e.g., the classification of finite abelian groups, or one can view these groups as vector spaces over F_2.Completed by @Alex Meiburg
B.2. Homomorphism counting Again, some of the group theory API (e.g., isomorphism theorems) may be helpful here. Completed by @Alex Meiburg
B.3. Slicing This is a double counting argument, should be straightforward Completed by @Terence Tao
B.4. Linearization of approximate homomorphisms This one should also be straightforward. Completed by @Terence Tao

As usual, feel free to "claim" any of the tasks as a response to this thread!

[Yaël Dillies]

I will take on "B.1. Duality of finite abelian 2-groups" since I've already got the pieces in APAP

[Pietro Monticone]

Both @Lorenzo Luccioli and I are currently too busy to take on this task, so please feel free to disclaim it.

[Terence Tao]

Pietro Monticone said:

Both Lorenzo Luccioli and I are currently too busy to take on this task, so please feel free to disclaim it.

OK, I've done so. I notice you do have a small PR on this already with a modest start in the task and some styling changes. Is it worth getting that mergeable, or should one abandon that PR entirely?

[Pietro Monticone]

I think we should abandon that PR entirely.

[Terence Tao]

I'll take A.1-A.4 (I'm curious to see whether AI tools are of any help here for transferring between somewhat similar tasks).

[Terence Tao]

Finished A.1. I was rusty (especially with regards to how iIndepFun and indepFun interacted) and it took about four hours. Annoyingly, I spent a ridiculous amount of time proving the utterly trivial fact that a set and its complement were pairwise disjoint:

import Mathlib

example (A: Type) [Fintype A] [DecidableEq A] (S: Finset A) : Set.univ.PairwiseDisjoint (fun
| 0 => S
| 1 => Sᶜ
: Fin 2 → Finset A):= by
  intro a _ b _ hab
  simp [Function.onFun, ←le_compl_iff_disjoint_left]
  match a, b with
  | 0, 0 => simp at hab
  | 0, 1 => simp
  | 1, 0 => simp
  | 1, 1 => simp at hab

Presumably there is an easier way to do this.

[Aaron Liu]

import Mathlib

example {A : Type*} [Fintype A] [DecidableEq A] (S : Finset A) : Set.univ.PairwiseDisjoint ![S, Sᶜ] := by
  rw [Set.PairwiseDisjoint, Set.Pairwise]
  simp_rw [Fin.forall_fin_two]
  simp [Function.onFun, disjoint_compl_left, disjoint_compl_right]

[Terence Tao]

Thanks! This is now incorporated.

Formalized A.2 in about an hour (it was a "three line proof" in the blueprint, but about 25 lines in Lean). Github Copilot has some minor utility, for instance in speeding up various search-and-replace type tasks, and giving the skeleton of proof of one lemma if one has already proven a similar lemma, but certainly not as impactful as it was for simpler problems (such as the ones I did on Youtube).

[Terence Tao]

In case anyone is interested, I made a video of how A.2 was formalized: https://www.youtube.com/watch?v=6uLXA9KROBg

[Terence Tao]

Finished A.3, in about four hours as well. One strange sticking point was embedding sums over Fin m into sums over Fin (m+1). I spent a non-trivial amount of time on this silly lemma:

import Mathlib

lemma Finset.sum_extend {H:Type*} [AddCommMonoid H] {m:ℕ} (f: Fin (m+1) → H) : ∑ i : Fin m, f i = ∑ i < (m: Fin (m+1)), f i := calc
        _ = ∑ i : Fin m, f (Fin.castSuccEmb i) := by
          congr; ext i; congr
          simp only [Fin.coe_eq_castSucc, Fin.coe_castSuccEmb]
        _ = ∑ i ∈ Finset.map Fin.castSuccEmb Finset.univ, f i := by
          exact (Finset.sum_map  _ _ _).symm
        _ = _ := by
          congr
          simp only [Fin.natCast_eq_last, Fin.Iio_last_eq_map]

Perhaps there is a better way to do this.

[Aaron Liu]

docs#Fin.sum_univ_castSucc

[Aaron Liu]

I honestly didn't think this would work

import Mathlib

lemma Finset.sum_extend {H : Type*} [AddCommMonoid H] {m : ℕ}
    (f : Fin (m + 1) → H) : ∑ i : Fin m, f i = ∑ i < (m : Fin (m + 1)), f i := by
  simp

[Terence Tao]

Wow, I can't believe I didn't try that. Thanks!

[Sébastien Gouëzel]

When a simp call works unexpectedly like that, a good idea is to look at the output of simp? to see where the miracle is coming from. Here, the key is docs#Fin.Iio_last_eq_map

[Kim Morrison]

Terence Tao said:

Wow, I can't believe I didn't try that. Thanks!

Hopefully one day (soon-ish?) as soon as you type by various tactics will start running in the background, and it will become impossible to miss things like this...

[Terence Tao]

Finished A.4, after about five hours of work; this was the most complex of the four tasks I had claimed. Some observations:

• It was useful to get the high-level structure of the argument in place first, leaving all the side conditions as sorries to be filled in later. For instance, the human proof at pfr#multidist-ruzsa-IV was a bunch of entropy inequalities and equalities to be combined together, which initially suggested using a long calc block with some adding and subtracting using abel, congr, and gcongr or ring as connective tissue; but it turned out to be simpler to just make each of the entropy (in)equality inputs as a have statement (proven initially by a sorry) and close the argument with linarith rather than figure out exactly how to arrange the pieces together as a calc. The other advantage of doing the high level part first is that one could group together all the similar sorries (e.g., a bunch of side claims about what random variables were independent to what other ones), at which point one could more easily see how to prove them together.
• In the latter regard, Github Copilot was useful in filling out the proof of many of these similar side conditions, once one had written a proof of one of them by hand. Its error rate in doing so was still non-zero, but low enough that it was a net win to have Copilot fill in dozens of lines of code and then spot fix the one or two lines that weren't quite right. However, copilot fared significantly worse when it did not have such a reference proof to serve as a model. On the other hand, it was useful for fixing some more basic issues I had with portions of Lean syntax that I was not extensively familiar with.
• I am still learning the lesson that many small arguments used inside the proof of one lemma should in fact be abstracted out as a more general lemma to be reused in proving later lemmas (one example of this is in the above video where I moved several small lemmas about off-diagonal sums into the global namespace). In particular there is a lot of redundancy across PFR in the task of showing that various combinations of independent random variables remain independent, which could be done more systematically and efficiently, but the code is compiling now (well, there was one small issue I saw this morning, but I pushed a fix) and cleaning up the code is low priority. (In fact the optimal strategy here may just be to wait until the AI tools get to the point where they can semi-automatically do such refactoring for us.)
• The measurability tactic is powerful and convenient, but consumes a lot of heartbeats. I used it extensively at the beginning, but later replaced many such invocations with more explicit proofs, trading brevity of the proof for reduced heartbeat usage. It would be nice to have a measurability? tactic to do this automatically.
• There was a small hole in the API for identical distribution that needed a new lemma: if $(X_i)_{i \in I}, (X'_i)_{i \in I}$ are tuples of jointly independent variables with $X_i$ identically distributed to $X'_i$ for each $i$, then $(X_i)_{i \in I}$ is identically distributed with $(X'_i)_{i \in I}$. We had this for pairs, but not for more general (countable) tuples. It wasn't super difficult (see proof below), but rather different from the rest of the formalization task at hand, so I am glad that I adopted a "high level first" approach which allowed me to defer this task to the very end.

theorem IdentDistrib.iprodMk {I: Type*} [Fintype I] {F : I → Ω → β} {F' : I → Ω' → β} (hFF': ∀ i, IdentDistrib (F i) (F' i) μ ν) (hμ: IsProbabilityMeasure μ) (hν: IsProbabilityMeasure ν) (h : iIndepFun F μ) (h' : iIndepFun F' ν) :
    IdentDistrib (fun x i ↦ F i x) (fun x i ↦ F' i x) μ ν where
  aemeasurable_fst := by
    apply AEMeasurable.piMk
    intro i; exact (hFF' i).aemeasurable_fst
  aemeasurable_snd := by
    apply AEMeasurable.piMk
    intro i; exact (hFF' i).aemeasurable_snd
  map_eq := by
    rw [iIndepFun_iff_map_fun_eq_pi_map] at h h'
    . rw [h,h']
      congr
      ext i : 1
      exact (hFF' i).map_eq
    . intro i; exact (hFF' i).aemeasurable_snd
    intro i; exact (hFF' i).aemeasurable_fst

[Terence Tao]

It took the better part of a day, but A.6 is now also formalized. My experience was very similar to that for A.4. There were a number of steps that were trivial in the informal proof of this "Corollary" due to things like the obvious identification between G and Fin 1 → G, so various congr and comp type API for things like multidistance, entropy, and conditional mutual information needed to be written first (I have placed them just before the proof of the main A.6 theorem; in principle one could reorganize the codebase to be more logical, but the PFR project is nearly completed and would probably need a major refactor in any event if one wanted to use the proofs here in some future project).

There were a large number of subtasks of the form "Show that these various combinations of the jointly independent random variables $X_{i,j}$ are themselves jointly independent". We have a useful tool for this, iIndepFun.finsets_comp (the PFR doc-gen is buggy and I don't think pfr#iIndepFun.finsets_comp is working properly, it cannot find https://teorth.github.io/pfr/docs/PFR/Mathlib/Probability/Independence/Basic.html#ProbabilityTheory.iIndepFun.finsets_comp), and I have some boilerplate code now to verify the various pairwise disjointness etc. hypotheses in about a dozen lines each time this subtask is required, but it would be nice to automate this more. (But Github Copilot does a good job of reproducing this boilerplate once it has one or two existing examples in the file.)

In contrast, the situation with the measurability side conditions (rather than the independence side conditions) is much better: tacking on <;> try fun_prop at the end of any tactic that generates such side conditions largely solves the problem and helps declutter the code (but it is still nearly 500 lines and consumes 400000 heartbeats).

There was one strange Lean anomaly I did not understand. At several points in the code I needed to simplify (f + g) x to f x + g x for various functions f, g. Strangely, simp refused to do this, even after explicitly adding

@[simp]
lemma fun_add {X:Type*} {G:Type*} [Add G] (f g: X → G) (x:X) : (f + g) x = f x + g x := rfl

Only rw [fun_add] worked; neither simp [fun_add] or simp_rw [fun_add] made progress. I suspect it is some strange dependent type issue (e.g., https://github.com/teorth/pfr/blob/master/PFR/MoreRuzsaDist.lean#L2208 is one location where this occurs).

[Terence Tao]

OK, I at least figured out the Lean anomaly. I had let a variable G' denote a function type, but because I did not explicitly unfold it during simp, simp did not recognize it as a function and so could not use fun_add. Adding G' to the simpset resolves the problem, and I can remove fun_add.

[Terence Tao]

Spent the last few days knocking off the smaller outstanding tasks. Project B is now completed, and of Project A, there are now just four outstanding tasks (with one of them currently in review as a PR). The final three are somewhat substantial, though.

[Sébastien Gouëzel]

Can I claim A.5?

[Terence Tao]

Of course!

[Terence Tao]

A.15 is now completed! Only two tasks are now outstanding in the entire project, of which both are claimed by others.

The formalization went smoothly, except for one wrong turn when I thought I had found a neat simplification, but it turned out to be wrong (I misidentified two different probability measures as being equal), and one place where I needed two different MeasureSpace structures on the same space (due to conditioning a probability measure) which required overriding the instance mechanism by explicitly passing some parameters. But I am getting one weird bug report: in the proof of pfr#k_eq_zero I get an "error"

Error in Linarith.normalizeDenominatorsLHS: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  2 *
    (d[U # U] + p.η / ↑p.m * ∑ i, d[X i # U] -
      ((2 + p.η / ↑p.m * ↑p.m / 2) * (I[Z1 : Z2 ; μ] + I[Z1 : Z3 ; μ] + I[Z2 : Z3 ; μ]) +
        p.η / ↑p.m * ∑ i, d[X i ; ℙ # Z2 ; μ]))
-- lots of proof state omitted
⊢ ?m.361550

which doesn't seem to actually prevent elaboration. I suspect that linarith is struggling with some defeq abuse that I relied on to make the proof work, but I'm not sure exactly what the issue is. (There are other places in the proof where I had to use convert instead of apply or exact, again probably due to defeq abuse, and maybe having to do with overriding some instances.) It would be nice to debug this, but technically the proof passes CI, so I guess all is well that ends well?

[Sébastien Gouëzel]

PR for A.5 at https://github.com/teorth/pfr/pull/254

[Terence Tao]

image.png
image.png
Projects A and B have now been completely formalized, making the PFR repository fully sorry-free! Thanks to all the contributors to the PFR project for all their efforts!

[Yaël Dillies]

Now is high time to upstream then :innocent:

[Terence Tao]

Ah, that reminds me, there are some helper lemmas (mostly regarding independence and identical distribution) that I had to wrote for the torsion endgame that I should at least move to an appropriate ForMathlib folder.