English
The increment partition has a prescribed size: the number of its parts equals stepBound(#P.parts) under suitable assumptions and if P is not uniform.
Русский
У приращивающее разбиение имеет заданный размер: число его частей равно stepBound(#P.parts) при некоторых условиях и если P не является равномерным.
LaTeX
$$$\\#(increment\\, hP\\, G\\, \\varepsilon).parts = \\mathrm{stepBound}(\\#P.parts)$$$
Lean4
/-- The **increment partition** in Szemerédi's Regularity Lemma.
If an equipartition is *not* uniform, then the increment partition is a (much bigger) equipartition
with a slightly higher energy. This is helpful since the energy is bounded by a constant (see
`Finpartition.energy_le_one`), so this process eventually terminates and yields a
not-too-big uniform equipartition. -/
noncomputable def increment : Finpartition (univ : Finset α) :=
P.bind fun _ => chunk hP G ε
