Numerical bounds for Szemerédi Regularity Lemma #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file gathers the numerical facts required by the proof of Szemerédi's regularity lemma.
This entire file is internal to the proof of Szemerédi Regularity Lemma.
Main declarations #
Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean
Auxiliary function for Szemerédi's regularity lemma. Blowing up a partition of size
the induction results in a partition of size at most
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