initialBound — Mathlib

English

The initial bound is defined by the expression max(7, floor(log(100/ε^5)/log 4) + 1, l).

Русский

Начальная граница задаётся как максимум из 7, floor(log(100/ε^5)/log 4) + 1 и l.

LaTeX

$$$\mathrm{initialBound}(\varepsilon, l) = \max\{7, \; l, \; \left\lfloor \dfrac{\log(100/\varepsilon^{5})}{\log 4} \right\rfloor + 1\}$$$

Lean4

/-- Auxiliary function for Szemerédi's regularity lemma. The size of the partition by which we start
blowing. -/
noncomputable def initialBound : ℕ :=
  max 7 <| max l <| ⌊log (100 / ε ^ 5) / log 4⌋₊ + 1

Похожие утверждения