clog_of_right_le_zero — Mathlib

English

If r ≤ 0, then clog(b, r) = -log(b, r).

Русский

Если r ≤ 0, то clog(b, r) = -log(b, r).

LaTeX

$$$\operatorname{clog}(b,r) = -\log(b,r)$$$

Lean4

theorem clog_of_right_le_zero (b : ℕ) {r : R} (hr : r ≤ 0) : clog b r = 0 :=
  by
  rw [clog, if_neg (hr.trans_lt zero_lt_one).not_ge, neg_eq_zero, Int.natCast_eq_zero, Nat.log_eq_zero_iff]
  rcases le_or_gt b 1 with hb | hb
  · exact Or.inr hb
  · refine Or.inl (lt_of_le_of_lt ?_ hb)
    exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)

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