Outstanding tasks, version 5.0

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

Yet another rollover of the "outstanding tasks" thread. The previous thread can be found here.

While the primary aims of the PFR project are nearly complete, I'm now adding a few mostly expository tasks to the queue to help showcase the achievements of the project to outsiders. Following a suggestion of @Thomas Bloom , I have also just written a quick blueprint to formalize a consequence of the PFR conjecture that is used by computer scientists, as well as stubs of lemmas in https://github.com/teorth/pfr/blob/master/PFR/homomorphism.lean , but it is very rudimentary and in particular even the statements of the lemmas (not just the proofs) need formalizing. [EDIT: the statements are now formalized.]

A. Existing claims:

1. @Yaël Dillies and @Bhavik Mehta have established Entropic Balog-Szemeredi-Gowers (and also claim combinatorial Balog-Szemeredi-Gowers, which is currently not covered by the Blueprint)
2. @Paul Lezeau and @Jonas Bayer claim Bound on distance increments

B. Outstanding proof formalization tasks:

1. Hahn-Banach type theorem This should be a routine induction on the order of the group (there may also be a slick homological algebra proof). Established by @Adam Topaz
2. Goursat type theorem This is a mostly algebraic lemma, which will also require an induction on the order of the group at some point. Established by @llllvvuu
3. Homomorphism form of PFR A reasonably straightforward application of PFR to a graph of a function, manipulating homomorphisms and subgroups in simple ways, and using the previous two lemmas. Established by @Arend Mellendijk

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

1. Writing examples to illustrate probability kernels.
2. Writing examples to illustrate Shannon entropy. Established by @Terence Tao
3. Writing examples to illustrate Ruzsa distance. Established by @Terence Tao
4. Writing examples to illustrate the finiteness tactic. Established by @Terence Tao
5. Writing examples to illustrate real-valued measures. Established by @Terence Tao
6. Formalizing the statement of Hahn-Banach type theorem Established by @Terence Tao
7. Formalizing the statement of Goursat type theorem Established by @Terence Tao
8. Formalizing the statement of Homomorphism form of PFR Established by @Terence Tao

D. Outstanding administrative tasks: none currently

Note: one can of course simultaneously claim the task of formalizing the statement of a lemma, and also proving it.

[Jonas Bayer]

The file endgame.lean introduces notation for variables using the notation3 command. Wouldn't it be better to just define them using def or abbrev? Earlier I tried instantiating a lemma from a different file and had to explicitly provide the argument S. But that wasn't possible since S is custom notation...

[Kyle Miller]

If, for example, you made local notation3 "W" => X₁' + X₁ be a def, then you'd have to pass X₁' and X₁ to it, which defeats the purpose of defining it. The notation trick is how you can make W refer to these specific variables.

What problem are you running into? If you're in another module you shouldn't see S at all. You could copy all the local notation lines to that module if they make sense there, if you did want to refer to S.

[Terence Tao]

I've formalized the statement of the three lemmas needed to derive the homomorphism version of PFR from the combinatorial version. The first two are purely algebraic and could potentially be obtained in some slick fashion from existing homological algebra machinery (but I don't know how well developed that machinery is in Mathlib, and in any event I don't know how to wield homological algebra very well even at the informal level), but should also be provable by a brute force induction. The third result is hopefully not too challenging given all the other results as black boxes.

I also wrote up some examples for entropy, Ruzsa distance, and finiteness (where in the latter I mostly just copied from the existing unit tests for the tactic). It might be worth adding a few more examples to the latter in order to aid in further development of that tactic, if anyone has some good ideas for such examples in mind. I'll leave the example section for probability kernels and real-valued measures to others (presumably the people who worked the most on those sections will have some ideas for representative examples to illustrate the machinery).

[Adam Topaz]

The first lemma should be easy with docs#LinearMap.exists_leftInverse_of_injective if the project already has a ZMod 2-module structure on an elementary abelian 2 group. I looked around for a few minutes but didn't see one :-/

[Terence Tao]

Adam Topaz said:

The first lemma should be easy with docs#LinearMap.exists_leftInverse_of_injective if the project already has a ZMod 2-module structure on an elementary abelian 2 group. I looked around for a few minutes but didn't see one :-/

Ah, right, who needs homological algebra when linear algebra is available instead! :smile:

We have the reverse implication to what you say in pfr#ElementaryAddCommGroup.ofModule . So I guess one just has to work out the converse to pfr#ElementaryAddCommGroup.ofModule and apply docs#LinearMap.exists_leftInverse_of_injective to get task B.1. [The lazier option is to simply rewrite all the claims here in terms of modules instead of elementary 2-groups, but the converse sounds like a natural thing to prove anyway.] Unfortunately I can't attend to this any time soon, but hopefully someone will volunteer...

EDIT: task B.2 might also be treatable by this approach, though I don't know if the relevant lemma (about the existence of complementing vector subspaces) is already in Mathlib.

[Adam Topaz]

https://github.com/teorth/pfr/pull/119/files

[Adam Topaz]

It's still building on my end, so don't merge just yet :) Ok, it built successfully

[Adam Topaz]

Oof... endgame.lean takes quite a while to build!

[Terence Tao]

Adam Topaz said:

Oof... endgame.lean takes quite a while to build!

Hmm, maybe we need to do a stack trace and work out what is causing the delay? I have to sign off now unfortunately, but perhaps someone else can diagnose the issue.

[Adam Topaz]

It seems that there are already some comments in that file pointing to some slowness, e.g.

--(Mantas) this times out in the proof below
private lemma hmeas2 : Measurable
    (fun p : Fin 4 → G => ((p 0 + p 1, p 0 + p 2), p 0 + p 1 + p 2 + p 3)) := by measurability

[Terence Tao]

Adam Topaz said:

It seems that there are already some comments in that file pointing to some slowness, e.g.

--(Mantas) this times out in the proof below
private lemma hmeas2 : Measurable
    (fun p : Fin 4 → G => ((p 0 + p 1, p 0 + p 2), p 0 + p 1 + p 2 + p 3)) := by measurability

Ah, I also had discovered some slowness issues with measurability, see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/measurability.20tactic.20times.20out.20on.20Prod.2Efst.20.5Ccirc.20Prod.2Efst . Hopefully they can be fixed eventually, but a short-term fix I guess would just be to prove these measurability claims by hand.

[Jonas Bayer]

Kyle Miller said:

If, for example, you made local notation3 "W" => X₁' + X₁ be a def, then you'd have to pass X₁' and X₁ to it, which defeats the purpose of defining it. The notation trick is how you can make W refer to these specific variables.

What problem are you running into? If you're in another module you shouldn't see S at all. You could copy all the local notation lines to that module if they make sense there, if you did want to refer to S.

This makes sense, thank you for the explanation! The concrete problem that I was having was that I wanted to use the lemma iIndepFun.prod which Floris van Dorn had stated and that I inserted in the Independence file. It uses S as an implicit variable and

def myS : ... := ...
#check iIndepFun.prod (S := myS)

didn't work. I'm quite sure that this must be because of the notation since changing S to something else in iIndepFun.prod helped. Of course, for the final proof, one probably won't have to instantiate S explicitly. However, for exploration purposes, it is nice to have the possibility of incrementally building up the objects and hypotheses that get inserted in the theorem.

[Kyle Miller]

Oh, I misunderstood the problem you were running into from the short description of it. It's that since S is a local notation it's now a keyword, making it no longer be an identifier that you can use. That's annoying.

One option is to change the notation to use symbols that aren't identifiers. For example,

local notation3 "!V" => X₁' + X₂
local notation3 "!W" => X₁' + X₁
local notation3 "!S" => X₁ + X₂ + X₁' + X₂'
local notation3 "!I₁" => I[ !U : !V | !S ]

[Rémy Degenne]

I don't know what we should write about Markov kernels in the example file, and I think we might simply want to remove the section.

• Kernels are not defined in the project but in Mathlib. The project adds several simp lemmas and simple helper definitions that should be added to mathlib, but the theory of kernels is mostly from mathlib.
• The only significant result for kernels in the project is the disintegration of kernels in discrete measurable spaces (we only have it for constant kernels in mathlib) but in the discrete setting it's a direct consequence of the constant kernel case. The reason it's not in mathlib is that I want to add the general version in standard Borel spaces.
• What the project contains related to kernels are developments of entropy, mutual information and Ruzsa distance. But in the example file we probably don't want to talk about those: we should only mention simple properties of those objects for random variables, not for kernels.

[Rémy Degenne]

In summary, I don't think that the example file is the right place. I have started writing a blog post about the use of kernels for entropy and independence (conditional independence using kernels just landed in mathlib!). https://leanprover-community.github.io/blog/ could be the right place to talk about that.

[Terence Tao]

Rémy Degenne said:

In summary, I don't think that the example file is the right place. I have started writing a blog post about the use of kernels for entropy and independence (conditional independence using kernels just landed in mathlib!). https://leanprover-community.github.io/blog/ could be the right place to talk about that.

OK, I will remove the section.

[Jonas Bayer]

Today I managed to finish proving the independence condition necessary for establishing pfr#sum_dist_diff_le which you can find in this pr. I'd be very happy about any feedback on code style and how to simplify the proofs of ineq1, independenceCondition1 and independenceCondition1'. If these proofs can be shortened this would likely simplify the proofs of the remaining inequalities.

[llllvvuu]

I started to give goursat a shot (WIP: https://github.com/teorth/pfr/pull/125)

by the way, i'm seeing a build issue in endgame.lean which i just commented out for now

[llllvvuu]

goursat is complete

[Arend Mellendijk]

I'm making good progress towards the homomorphism form of PFR at the moment

[Arend Mellendijk]

And here it is!