log_of_one_le_right — Mathlib

English

If r ≥ 1, then log(b,r) equals the integer cast of the floor of log base b of floor(r).

Русский

Если r ≥ 1, то log(b,r) равно целочисленному приведения к целому от floor логарифма по основанию b от floor(r).

LaTeX

$$$\forall {R} [\text{Semifield } R] [\text{LinearOrder } R] [\text{FloorSemiring } R] (b : \mathbb{N}) (r : R), (1 \le r) \Rightarrow \log(b,r) = \text{cast}(\log_b(\lfloor r \rfloor_+))$$$

Lean4

theorem log_of_one_le_right (b : ℕ) {r : R} (hr : 1 ≤ r) : log b r = Nat.log b ⌊r⌋₊ :=
  if_pos hr

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