Szemerédi's Regularity Lemma #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
such that the resulting partitioned graph is
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
The proof we formalise goes as follows:
- Define an auxiliary measure of edge density, the energy of a partition.
- Start with an arbitrary equipartition of size
- 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-
- Check that this results in an equipartition with an energy greater than the energy of the current partition, plus some constant.
- Since the energy is between zero and one, we can't run this process forever. Check that when the
process stops we have an
This file only contains the final result. The supporting material is spread across the
combinatorics.simple_graph.regularity.bound: Definition of the bound on the number of parts. Numerical inequalities involving the lemma constants.
combinatorics.simple_graph.regularity.energy: Definition of the energy of a simple graph along a partition.
combinatorics.simple_graph.regularity.uniform: Definition of uniformity of a simple graph along a pair of parts and along a partition.
combinatorics.simple_graph.regularity.equitabilise: Construction of an equipartition with a prescribed number of parts of each size and almost refining a given partition.
combinatorics.simple_graph.regularity.chunk: Break up one part of the current equipartition. Check that density between non-uniform parts increases, and that density between uniform parts doesn't decrease too much.
combinatorics.simple_graph.regularity.increment: Gather all those broken up parts into the new equipartition (aka increment partition). Check that energy increases by at least a fixed amount.
combinatorics.simple_graph.regularity.lemma: Wrap everything up into an induction on the energy.
We currently only prove the equipartition version of SRL.
- Prove the diagonal version.
- Prove the degree version.
- Define the regularity of a partition and prove the corresponding version.
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).