Szemerédi's Regularity Lemma #

In this file, we prove Szemerédi's Regularity Lemma (aka SRL). This is a landmark result in combinatorics roughly stating that any sufficiently big graph behaves like a random graph. This is useful because random graphs are well-behaved in many aspects.

More precisely, SRL states that for any ε > 0 and integer l there exists a bound M such that any graph on at least l vertices can be partitioned into at least l parts and at most M parts such that the resulting partitioned graph is ε-uniform.

This statement is very robust to tweaking and many different versions exist. Here, we prove the version where the resulting partition is equitable (aka an equipartition), namely all parts have the same size up to a difference of 1.

The proof we formalise goes as follows:

  1. Define an auxiliary measure of edge density, the energy of a partition.
  2. Start with an arbitrary equipartition of size l.
  3. Repeatedly break up the parts of the current equipartition in a big but controlled number of parts. The key point is to break along the witnesses of non-uniformity, so that a lesser portion of the pairs of parts are non-ε-uniform.
  4. Check that this results in an equipartition with an energy greater than the energy of the current partition, plus some constant.
  5. Since the energy is between zero and one, we can't run this process forever. Check that when the process stops we have an ε-uniform equipartition.

This file only contains the final result. The supporting material is spread across the Combinatorics/SimpleGraph/Regularity folder:


We currently only prove the equipartition version of SRL.

References #

Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean

theorem szemeredi_regularity {α : Type u_1} [DecidableEq α] [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : } {l : } (hε : 0 < ε) (hl : l Fintype.card α) :
∃ (P : Finpartition Finset.univ), P.IsEquipartition l SzemerediRegularity.bound ε l P.IsUniform G ε

Effective Szemerédi Regularity Lemma: For any sufficiently large graph, there is an ε-uniform equipartition of bounded size (where the bound does not depend on the graph).