English
There is an equality relating clog and inverse via log, namely clog(b, r^{-1}) = -log(b, r).
Русский
Связь clog и обратного через логарифм: clog(b, r^{-1}) = -log(b, r).
LaTeX
$$$\operatorname{clog}(b, r^{-1}) = -\log(b, r)$$$
Lean4
@[simp]
theorem clog_inv (b : ℕ) (r : R) : clog b r⁻¹ = -log b r :=
by
rcases lt_or_ge 0 r with hrp | hrp
· obtain hr | hr := le_total 1 r
· rw [clog_of_right_le_one _ (inv_le_one_of_one_le₀ hr), log_of_one_le_right _ hr, inv_inv]
· rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]
· rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]
