beattySeq' — Mathlib

English

The Beatty complement Beatty complement sequence beattySeq' is defined by beattySeq'(r,k) = ceil(k r) - 1.

Русский

Дополнительная последовательность Битти beattySeq' определяется как beattySeq'(r,k) = ceil(k r) - 1.

LaTeX

$$$beattySeq'(r,k) = \\lceil k r \\rceil - 1$$$

Lean4

/-- In this variant of the Beatty sequence for `r`, the `k`th term is `⌈k * r⌉ - 1`. -/
noncomputable def beattySeq' (r : ℝ) : ℤ → ℤ := fun k ↦ ⌈k * r⌉ - 1

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