log_mod_opow_log_lt_log_self — Mathlib

English

If hb > 1 and o ≥ log b o, then log b (o mod (b^{log b o})) < log b o.

Русский

Если hb > 1 и o ≥ log_b o, тогда log_b (o mod (b^{log_b o})) < log_b o.

LaTeX

$$$ \log_b (o \% (b^{\log_b o})) < \log_b o $$$

Lean4

theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (hbo : b ≤ o) : log b (o % (b ^ log b o)) < log b o :=
  by
  rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h
  · rw [h, log_zero_right]
    exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo
  · rw [← succ_le_iff, succ_log_def hb h]
    apply csInf_le'
    apply mod_lt
    rw [← Ordinal.pos_iff_ne_zero]
    exact opow_pos _ (zero_lt_one.trans hb)

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