English
If G is LocallyLinear and ε>0, then (G.cliqueFinset 3) is nonempty.
Русский
Если граф G локально линейный и ε>0, то множество тройк кликов не пусто.
LaTeX
$$G.LocallyLinear → (G.cliqueFinset 3).Nonempty$$
Lean4
/-- An explicit form for the constant in the triangle removal lemma.
Note that this depends on `SzemerediRegularity.bound`, which is a tower-type exponential. This means
`triangleRemovalBound` is in practice absolutely tiny.
This definition is meant to be used for small values of `ε`, and in particular is junk for values
of `ε` greater than or equal to `1`. The junk value is chosen to be positive, so that
`0 < ε → 0 < triangleRemovalBound ε` regardless of whether `ε < 1` or not. -/
noncomputable def triangleRemovalBound (ε : ℝ) : ℝ :=
min (2 * ⌈4 / ε⌉₊ ^ 3)⁻¹ ((1 - min 1 ε / 4) * (ε / (16 * bound (ε / 8) ⌈4 / ε⌉₊)) ^ 3)
