natFloor_logb_natCast — Mathlib

English

For natural base b and natural n, ⌊log_b(b.cast n.cast)⌋₊ = Nat.log b n.

Русский

Для натурального основания b и натурального n, ⌊log_b b.cast n.cast⌋₊ = Nat.log b n.

LaTeX

$$⌊logb b.cast n.cast⌋₊ = Nat.log b n$$

Lean4

@[norm_cast]
theorem natFloor_logb_natCast (b : ℕ) (n : ℕ) : ⌊logb b n⌋₊ = Nat.log 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_floor_eq_floor, floor_logb_natCast (by simp), Int.log_natCast]
  exact logb_nonneg (by simp [Nat.cast_add_one_pos]) (Nat.one_le_cast.2 (by cutsat))

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