nValue

Mathlib.Combinatorics.Additive.AP.Three.Behrend

URI: https://scilib.ai/kg/mathlib#Behrend.nValue

English

For N ∈ ℕ, Behrend's nValue(N) is defined as ⌈√(ln N)⌉.

Русский

Для натурального N функция Behrend nValue(N) задаётся как ⌈√(ln N)⌉.

LaTeX

$$$$ nValue(N) = \\lceil \\sqrt{\\log N} \\rceil. $$$$

Lean4

/-- The (almost) optimal value of `n` in `Behrend.bound_aux`. -/
noncomputable def nValue (N : ℕ) : ℕ :=
  ⌈√(log N)⌉₊

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru