English
bound(ε, l) is defined as a product of a stepBound iteration and a power of 16, with stepBound computed from initialBound.
Русский
bound(ε, l) задаётся как произведение итерации stepBound и степени 16, где stepBound определяется через initialBound.
LaTeX
$$$\mathrm{bound}(\varepsilon, l) = (\mathrm{stepBound}^{\!\!\,[\lfloor 4/\varepsilon^{5} \rfloor \!\!\!]} (\mathrm{initialBound}(\varepsilon, l))) \cdot 16^{(\mathrm{stepBound}^{\!\!\,[\lfloor 4/\varepsilon^{5} \rfloor \!\!\!]} (\mathrm{initialBound}(\varepsilon, l)))}$$$
Lean4
/-- An explicit bound on the size of the equipartition whose existence is given by Szemerédi's
regularity lemma. -/
noncomputable def bound : ℕ :=
(stepBound^[⌊4 / ε ^ 5⌋₊] <| initialBound ε l) * 16 ^ (stepBound^[⌊4 / ε ^ 5⌋₊] <| initialBound ε l)
