English
For hb: 1 < b, x ≤ y ↔ clog b x ≤ y.
Русский
Для hb: 1 < b выполняется x ≤ y ↔ clog_b(x) ≤ y.
LaTeX
$$$ (1 < b) \Rightarrow x \le y \iff \operatorname{clog}(b,x) \le y $$$
Lean4
/-- `clog b` and `pow b` form a Galois connection. -/
theorem clog_le_iff_le_pow {b : ℕ} (hb : 1 < b) {x y : ℕ} : clog b x ≤ y ↔ x ≤ b ^ y :=
by
induction x using Nat.strong_induction_on generalizing y with
| h x ih => ?_
cases y
· rw [Nat.pow_zero]
refine ⟨?_, fun h => (clog_of_right_le_one h b).le⟩
simp_rw [← not_lt]
contrapose!
exact clog_pos hb
have b_pos : 0 < b := zero_lt_of_lt hb
rw [clog]; split_ifs with h
·
rw [Nat.add_le_add_iff_right, ih ((x + b - 1) / b) (add_pred_div_lt hb h.2), Nat.div_le_iff_le_mul_add_pred b_pos,
Nat.mul_comm b, ← Nat.pow_succ, Nat.add_sub_assoc (Nat.succ_le_of_lt b_pos), Nat.add_le_add_iff_right]
· exact iff_of_true (zero_le _) ((not_lt.1 (not_and.1 h hb)).trans <| succ_le_of_lt <| Nat.pow_pos b_pos)
