English
The cornersTheoremBound is an explicit, noncomputable function that, for a given ε > 0, produces a natural number bounding the size of the ambient group in the corners theorem. It depends on a tower-type Szemerédi bound but is, in practice, an extremely small constant.
Русский
Функция cornersTheoremBound является явной, невычислимой константой, которая задаёт константу границы теоремы углов в зависимости от ε и связана со значением Szemerédi bounds; на практике она чрезвычайно малая.
LaTeX
$$$\text{cornersTheoremBound}: \mathbb{R} \to \mathbb{N},\quad \text{cornersTheoremBound}(\varepsilon) = \Big\lfloor (\triangleRemovalBound(\varepsilon/9) \cdot 27)^{-1} \Big\rfloor_+ + 1.$$$
Lean4
/-- An explicit form for the constant in the corners theorem.
Note that this depends on `SzemerediRegularity.bound`, which is a tower-type exponential. This means
`cornersTheoremBound` is in practice absolutely tiny. -/
noncomputable def cornersTheoremBound (ε : ℝ) : ℕ :=
⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ + 1
