English
If r ≤ 1, then log(b,r) equals the negated ceiling of the logarithm of the reciprocal, i.e. −clog b ⌈r⁻¹⌉₊ cast to integers.
Русский
Если r ≤ 1, то log(b,r) равно −clog b ⌈r⁻¹⌉₊, приводимому к целому.
LaTeX
$$$\forall {R} [\text{Semifield } R] [\text{LinearOrder } R] [\text{FloorSemiring } R] (b : \mathbb{N}) (r : R), r \le 1 \Rightarrow \log(b,r) = -\mathrm{clog}(b, \lceil r^{-1} \rceil_+).cast$$$
Lean4
theorem log_of_right_le_one (b : ℕ) {r : R} (hr : r ≤ 1) : log b r = -Nat.clog b ⌈r⁻¹⌉₊ :=
by
obtain rfl | hr := hr.eq_or_lt
·
rw [log, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right, Int.ofNat_zero,
neg_zero]
· exact if_neg hr.not_ge
