add_log_le_log_mul — Mathlib

English

For x,y ≠ 0 and base b, log_b x + log_b y ≤ log_b (x y).

Русский

Для x,y ≠ 0 и основания b выполняется log_b x + log_b y ≤ log_b (x y).

LaTeX

$$$ \log_b x + \log_b y \le \log_b (x y) $$$

Lean4

theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y ≠ 0) :
    log b x + log b y ≤ log b (x * y) := by
  obtain hb | hb := lt_or_ge 1 b
  · rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)
  · simpa only [log_of_left_le_one hb, zero_add] using le_rfl

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