Numerical bounds for Szemerédi Regularity Lemma #
This file gathers the numerical facts required by the proof of Szemerédi's regularity lemma.
Main declarations #
Auxiliary function for Szemerédi's regularity lemma. Blowing up a partition of size
the induction results in a partition of size at most
Alias of the reverse direction of szemeredi_regularity.step_bound_pos_iff`.
Auxiliary function for Szemerédi's regularity lemma. The size of the partition by which we start
An explicit bound on the size of the equipartition whose existence is given by Szemerédi's