English
If m ≠ 0, then the number of parts of chunk hP G ε hU is 4^{|P.parts|}.
Русский
Если m ≠ 0, то число частей chunk hP G ε hU равно 4^{|P.parts|}.
LaTeX
$$$\#(\mathrm{chunk}\; hP\; G\; ε\; hU).\mathrm{parts} = 4^{\#P.parts}$$$
Lean4
/-- The portion of `SzemerediRegularity.increment` which partitions `U`. -/
noncomputable def chunk : Finpartition U :=
if hUcard : #U = m * 4 ^ #P.parts + (card α / #P.parts - m * 4 ^ #P.parts) then
(atomise U <| P.nonuniformWitnesses G ε U).equitabilise <| card_aux₁ hUcard
else (atomise U <| P.nonuniformWitnesses G ε U).equitabilise <| card_aux₂ hP hU hUcard