English
For a natural base b > 1 and real r ≥ 0, ⌊log_b r⌋ = Int.log b r.
Русский
Для натурального основания b > 1 и вещественного r ≥ 0, ⌊log_b r⌋ = Int.log b r.
LaTeX
$$$b>1,\ r \ge 0 : \left\lfloor \log_b r \right\rfloor = \operatorname{Int}.log b r$$$
Lean4
@[norm_cast]
theorem floor_logb_natCast {b : ℕ} {r : ℝ} (hr : 0 ≤ r) : ⌊logb b r⌋ = Int.log b r :=
by
obtain rfl | hr := hr.eq_or_lt
· rw [logb_zero, Int.log_zero_right, Int.floor_zero]
by_cases hb : 1 < b
· have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
apply le_antisymm
· rw [← Int.zpow_le_iff_le_log hb hr, ← rpow_intCast b]
refine le_of_le_of_eq ?_ (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr)
exact rpow_le_rpow_of_exponent_le hb1'.le (Int.floor_le _)
· rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_intCast]
exact Int.zpow_log_le_self hb hr
· rw [Nat.one_lt_iff_ne_zero_and_ne_one, ← or_iff_not_and_not] at hb
cases hb
· simp_all only [CharP.cast_eq_zero, logb_zero_left, Int.floor_zero, Int.log_zero_left]
· simp_all only [Nat.cast_one, logb_one_left, Int.floor_zero, Int.log_one_left]
