log_anti_left — Mathlib

English

For a fixed n, the map b ↦ log_b n is antitone on the interval (1, ∞).

Русский

Для фиксированного n функция b ↦ log_b n убывает по основанию на промежутке (1, ∞).

LaTeX

$$$ (\forall n)\; \text{AntitoneOn}(\lambda b. \log_b n)(\mathrm{Ioi}(1)) $$$

Lean4

theorem log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n :=
  by
  rcases eq_or_ne n 0 with (rfl | hn); · rw [log_zero_right, log_zero_right]
  apply le_log_of_pow_le hc
  calc
    c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
    _ ≤ n := pow_log_le_self _ hn

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