natCeil_logb_natCast — Mathlib

English

Let b and n be natural numbers. The natural ceiling of log base b of n equals the base-b counting function of n.

Русский

Пусть b и n натуральны. Натуральный потолок log_b(n) равен clog_b(n).

LaTeX

$$$\lceil \log_b n \rceil_+ = \operatorname{clog}_b n$$$

Lean4

@[norm_cast]
theorem natCeil_logb_natCast (b : ℕ) (n : ℕ) : ⌈logb b n⌉₊ = Nat.clog b n :=
  by
  obtain _ | _ | b := b
  · simp [Real.logb]
  · simp [Real.logb]
  obtain rfl | hn := eq_or_ne n 0
  · simp
  rw [← Nat.cast_inj (R := ℤ), Int.natCast_ceil_eq_ceil, ceil_logb_natCast (by simp), Int.clog_natCast]
  exact logb_nonneg (by simp [Nat.cast_add_one_pos]) (Nat.one_le_cast.2 (by cutsat))

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