Szemerédi Regularity Lemma

Stream: PR reviews

[Yaël Dillies]

After more than a year, we finally hit the heart of the proof of Szemerédi Regularity Lemma. I've opened:

• #18368: Local positivity extension for SRL
• #18371: Partition a part in the main inductive argument of SRL

[Yaël Dillies]

My understanding is that positivityextensions are significantly harder to write in mathlib4, but this extension I am adding in #18368 really helped declutter the proofs in #18371. Also, it is a very basic positivity extension, supplying positivity proofs by looking for a few very common SRL-specific assumptions in the context.

[Yaël Dillies]

Thoughts, @Mario Carneiro?

[Mario Carneiro]

What kind of thoughts are you after? It should hopefully be possible to copy-paste your way through a positivity extension at this point

[Yaël Dillies]

I mean, do you want me not to write my SRL-specific extension or are you happy with me going forward with #18368?