Szemerédi's Theorem

Stream: graph theory

[Yaël Dillies]

Bhavik and I are gonna formalise Szemerédi's Theorem over the summer. Wish us luck!

[Yaël Dillies]

@Mauricio Collares, we're currently working on Szemerédi' Regularity Lemma here. There's not much to do at the moment as Bhavik is carrying the main induction and it's a bit one-goaled, but if you're still interested you can try to understand Gowers' proofs for when we actually start on it.

[Mauricio Collares]

Great! Thanks for letting me know and sorry for taking so long to reply. I was super busy (my deadline got extended by a few days) but now I have more free time. I will study Gowers' proof, hopefully I'll be able to help :)

[Yaël Dillies]

We have a bunch of constructions on simple_graph like

def is_uniform (ε : ℝ) (U W : finset α) : Prop :=
∀ U', U' ⊆ U → ∀ W', W' ⊆ W → ε * U.card ≤ U'.card → ε * W.card ≤ W'.card →
abs (edge_density G U' W' - edge_density G U W) < ε

Do you want me to PR them?

[Kyle Miller]

Yaël Dillies said:

Do you want me to PR them?

I think a good rule of thumb is that if formalized definitions have been tested by (partially) formalizing something else, then yes! I assume you have some sense of whether this works well for your application.

[Bhavik Mehta]

I think this definition is somewhat special to Szemeredi's regularity lemma and quasi-random properties of graphs, so probably should go in a new file (which probably will eventually contain the proof of SRL)