additive ramsey theory

Stream: maths

[David Wärn]

In branch#deuber/src/combinatorics/deuber.lean there is now a proof of "partition regularity of (m,p,c)-sets" (which is a sort of simultaneous generalisation of vdW and Folkman's theorem, and could become part of a proof of Rado's theorem). This was a bit tricky to formalise since there are a lot of details that you seem to need to do by hand. I'll try to PR it eventually.

[Yaël Dillies]

Oh very nice! Is it the same partition and regularity concepts as in branch#szemeredi/combinatorics/mathlib.lean? If so, I would very much like to compare approaches because I'm not quite happy with how we handle density (but it's more of an esthetic concern).

[Yaël Dillies]

cc @Bhavik Mehta

[Bhavik Mehta]

Yaël Dillies said:

Oh very nice! Is it the same partition and regularity concepts as in branch#szemeredi/combinatorics/mathlib.lean? If so, I would very much like to compare approaches because I'm not quite happy with how we handle density (but it's more of an esthetic concern).

The definitions can be read (in maths notation) from here https://dec41.user.srcf.net/h/III_L/ramsey_theory/3, I think David used an essentially equivalent source. The concept of regularity here is different, but partition means the same thing as it almost always does, except that in this case (like in most of combinatorics) we partition into finitely many bits.

[Yaël Dillies]

I've now had a look at branch#deuber, and it looks very good! Lots of cleanup to do and docstrings to be written, but I believe this is the way to go.