English
For a natural base b > 1 and real r ≥ 0, ⌈log_b r⌉ = Int.clog b r.
Русский
Для натурального основания b > 1 и вещественного r ≥ 0, ⌈log_b r⌉ = Int.clog b r.
LaTeX
$$$b>1,\ r \ge 0 : \lceil \log_b r \rceil = \operatorname{Int}.clog b r$$$
Lean4
@[norm_cast]
theorem ceil_logb_natCast {b : ℕ} {r : ℝ} (hr : 0 ≤ r) : ⌈logb b r⌉ = Int.clog b r :=
by
obtain rfl | hr := hr.eq_or_lt
· rw [logb_zero, Int.clog_zero_right, Int.ceil_zero]
by_cases hb : 1 < b
· have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
apply le_antisymm
· rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_intCast]
exact Int.self_le_zpow_clog hb r
· rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]
refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_
exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)
· 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.ceil_zero, Int.clog_zero_left]
· simp_all only [Nat.cast_one, logb_one_left, Int.ceil_zero, Int.clog_one_left]
