szemeredi_regularity

theorem szemeredi_regularity : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] {ε : ℝ} {l : ℕ}, 0 < ε → l ≤ Fintype.card α → ∃ P, P.IsEquipartition ∧ l ≤ P.parts.card ∧ P.parts.card ≤ SzemerediRegularity.bound ε l ∧ P.IsUniform G ε

The **Effective Szemerédi Regularity Lemma** states that for any sufficiently large graph represented by a simple graph `G` of type `α` (where `α` has decidable equality and is finite), there exists an `ε`-uniform equipartition `P` whose size is bounded and does not depend on the graph. Here, `ε` is a real number greater than zero and `l` is a natural number less than or equal to the cardinality of `α`. This equipartition `P` satisfies the following properties: it is an equipartition, has a number of parts equal to or greater than `l`, and less than or equal to the bound given by Szemerédi's Regularity Lemma for the parameters `ε` and `l`. Furthermore, `P` is uniform for the graph `G` with respect to `ε`.

More concisely: For any sufficiently large finite graph of type `α` with decidable equality, there exists an `ε`-uniform equipartition `P` of size bounded by Szemerédi's Regularity Lemma for parameters `ε` and `l`, having `l` or more parts and satisfying the uniformity condition for the graph.