posLog_nat_mul — Mathlib

English

Let n be a natural number and a real number a. Then log⁺(n·a) ≤ log n + log⁺ a.

Русский

Пусть n ∈ ℕ и a ∈ ℝ. Тогда log⁺(n a) ≤ log n + log⁺ a.

LaTeX

$$$\log^{+}(n a) \le \log n + \log^{+} a$$$

Lean4

/-- Estimate for `log⁺` of a product. Special case of `Real.posLog_mul` where one of
the factors is a natural number. -/
theorem posLog_nat_mul {n : ℕ} {a : ℝ} : log⁺ (n * a) ≤ log n + log⁺ a :=
  by
  rw [← log_of_nat_eq_posLog]
  exact posLog_mul

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