English
The function clog(b, r) is defined as the least integer power k such that r ≤ b^k when r > 0, and extends with a sign for negative r, via a complementary logarithm for the reciprocal.
Русский
Функция clog(b, r) определяется как наименьшее целочисленное показывающее степень k такое, что r ≤ b^k для r > 0; для отрицательных r применяется соответствующее представление через обратную величину.
LaTeX
$$$\operatorname{clog}(b,r) = \begin{cases} \mathrm{Nat\,clog}(b,\lceil r\rceil_+) & r>0, \\ -\mathrm{Nat\,log}(b,\lfloor r^{-1}\rfloor_+) & r>0, \end{cases}$$$
Lean4
theorem clog_of_one_le_right (b : ℕ) {r : R} (hr : 1 ≤ r) : clog b r = Nat.clog b ⌈r⌉₊ :=
if_pos hr
