dValue

Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

English

Behrend's dValue(N) = ⌊ N^{1/nValue(N)} / 2 ⌋.

Русский

Behrend dValue(N) = ⌊ N^{1/nValue(N)} / 2 ⌋.

LaTeX

$$$$ dValue(N) = \\Big\\lfloor \\frac{N^{1/nValue(N)}}{2} \\Big\\rfloor. $$$$

Lean4

/-- The (almost) optimal value of `d` in `Behrend.bound_aux`. -/
noncomputable def dValue (N : ℕ) : ℕ :=
  ⌊(N : ℝ) ^ (nValue N : ℝ)⁻¹ / 2⌋₊

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

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

Разделы

Аффилиация

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