beattySeq

Mathlib.NumberTheory.Rayleigh

URI: https://scilib.ai/kg/mathlib#beattySeq

English

The Beatty sequence for a real r is defined by beattySeq(r,k) = floor(k r).

Русский

Последовательность Битти для действительного r задаётся как beattySeq(r,k) = floor(k r).

LaTeX

$$$beattySeq(r,k) = \\lfloor k r \\rfloor$$$

Lean4

/-- In the Beatty sequence for real number `r`, the `k`th term is `⌊k * r⌋`. -/
noncomputable def beattySeq (r : ℝ) : ℤ → ℤ := fun k ↦ ⌊k * r⌋

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

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

Разделы

Аффилиация

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