Proof of `Szemerédi's regularity lemma`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The proof translates mathlib's equitable uniform partition into the indexed partition and non-strict regularity conventions used by this submission.
Proof strategy
Apply mathlib's effective equitable form of Szemerédi's regularity lemma, map its finite partition to the indexed partition used by the concept package, and transport equitability and regularity across the two definitions.
Attribution
The mathematical statement and energy-increment presentation follow Reinhard Diestel, Graph Theory, 5th edition, Section 7.4. The checked proof concludes the clean equipartition variant by translating the theorem formalized in mathlib by Yaël Dillies and Bhavik Mehta.