Outstanding tasks, version 8.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Time for another rollover! The previous outstanding tasks thread can be found here.

Now that entropy and Ruzsa distance is refactored to handle FiniteRange random variables rather than random variables taking values in a Fintype, we can begin to make more substantial progress on Chapter 11 of the blueprint (Weak PFR over the integers). In particular there are two preliminary lemmas (B.1 and B.2) that I had neglected to notice in the new blueprint whose statements are now formalized, and should be particularly easy to fill in, I think. For most of the remaining lemmas in the section (B.3-B.9), we need to first formalize the statements before proving them (tasks C.1-C.6, together with the two formalization tasks already claimed by @Paul Lezeau ).

A. Existing claims

1. @Yaël Dillies is gradually porting various stable PFR files over to Mathlib. Expect frequent Mathlib bumps during this process. It should be possible to work on extensions concurrently with this porting.
2. @Yaël Dillies and @Bhavik Mehta claim the proof of Balog-Szemeredi-Gowers
3. @Eric Rodriguez claims Approximate homomorphism form of PFR.
4. @Paul Lezeau claims the formalization of Torsion-free doubling and Torsion distance shrinking.
5. @Paul Lezeau claims the API for dimension.

B. Outstanding proof formalization tasks:

1. Distance from zero This should be an easy application of existing Ruzsa distance inequality machinery. Established by @Jonas Bayer
2. Fibring inequality This should be an easy corollary of General fibring identity and existing entropy machinery. Established by @Jonas Bayer
3. Projection entropy and distance An easy application of existing entropy inequalities.
4. Torsion-free doubling This is similar to many other entropy inequalities already in PFR, though somewhat lengthy. Awaits formalization.
5. Torsion distance shrinking Easy corollary of B.4. Awaits formalization.
6. Apply entropic PFR Easy application of existing PFR lemmas.
7. PFR projection One tricky thing is to locate a maximal subgroup H obeying a certain property, and show that the quotient is still an elementary abelian 2-group.
8. Single fibres Involves some manipulations of finite sums, but nothing too intimidating I think.
9. Asymmetric weak PFR Involves a strong induction, but should be doable.
10. Symmetric weak PFR Easy corollary of B.9.
11. Weak PFR over integers Easy corollary of B.9.

C. Outstanding documentation/blueprint/examples/statement formalization tasks:

1. Apply entropic PFR Should be straightforward to formalize. Completed by @Terence Tao
2. PFR projection Also straightforward. Completed by @Terence Tao
3. Single fibres A bit messy, but straightforward. Completed by @Terence Tao
4. Asymmetric weak PFR Straightforward to formalize. Completed by @Terence Tao
5. Symmetric weak PFR Also straightforward. Completed by @Terence Tao
6. Weak PFR over integers Also straightforward. Completed by @Terence Tao

D. Outstanding administrative tasks:

1. Add example showcasing weak PFR to examples.lean. Completed by @Terence Tao
2. Update HomPFR, ApproxHomPFR, examples.lean to accommodate the improvement of constants from 12 to 11. Completed by @Terence Tao

[Paul Lezeau]

By the way, just to avoid duplication of work, I should mention I'm also currently working on some API for dimension (and filling out the sorries)

[Jonas Bayer]

I'd like to claim 1. Distance from zero unless anyone else has started working on that.

[Jonas Bayer]

The claim is formalized with the additional assumption IsProbabilityMeasure μ'. Do we need the version with IsFiniteMeasure? This would require some API changes: entropy_const in a IsFiniteMeasure version and also a new Mathlib lemma that connects Measure.prod and multiplication of a measure by a constant.

[Jonas Bayer]

The proof is in https://github.com/TBUGTB/pfr, but before PRing I'd like to clean up some of the git history in my fork.

[Terence Tao]

(deleted)

[Terence Tao]

Jonas Bayer said:

The claim is formalized with the additional assumption IsProbabilityMeasure μ'. Do we need the version with IsFiniteMeasure? This would require some API changes: entropy_const in a IsFiniteMeasure version and also a new Mathlib lemma that connects Measure.prod and multiplication of a measure by a constant.

IsProbabilityMeasure should suffice for all PFR applications I think. If it can be cheaply extended to IsFiniteMeasure, that's great, but it's a somewhat low priority.

[Jonas Bayer]

It seems to me that the proof of B.3 (Projection entropy and distance) is a bit strange. For example, it wants to add up inequalities but there is only one.

My idea would be to move the lemma to the fibring file and use the Fibring inequality. Then it's just applying ent_of_indep_diff_lower and using that $U$ is uniform on $H$.

I.e. I'd like to claim B.3 and could also update the proof in the blueprint if that is helpful.