# 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:

- Define an auxiliary measure of edge density, the
*energy*of a partition. - Start with an arbitrary equipartition of size
`l`

. - 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. - 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
`ε`

-uniform equipartition.

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

folder:

`Combinatorics/SimpleGraph/Regularity/Bound`

: Definition of the bound on the number of parts. Numerical inequalities involving the lemma constants.`Combinatorics/SimpleGraph/Regularity/Energy`

: Definition of the energy of a simple graph along a partition.`Combinatorics/SimpleGraph/Regularity/Uniform`

: Definition of uniformity of a simple graph along a pair of parts and along a partition.`Combinatorics/SimpleGraph/Regularity/Equitabilise`

: Construction of an equipartition with a prescribed number of parts of each size and almost refining a given partition.`Combinatorics/SimpleGraph/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/SimpleGraph/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/SimpleGraph/Regularity/Lemma`

: Wrap everything up into an induction on the energy.

## TODO #

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.

## References #

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

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).