posLog_mul — Mathlib

English

log⁺ (a b) ≤ log⁺ a + log⁺ b.

Русский

log⁺ (ab) ≤ log⁺ a + log⁺ b.

LaTeX

$$log^{+}(ab) \le log^{+} a + log^{+} b$$

Lean4

/-- Estimate for `log⁺` of a product. See `Real.posLog_prod` for a variant involving
multiple factors. -/
theorem posLog_mul {a b : ℝ} : log⁺ (a * b) ≤ log⁺ a + log⁺ b :=
  by
  by_cases ha : a = 0
  · simp [ha, posLog]
  by_cases hb : b = 0
  · simp [hb, posLog]
  unfold posLog
  nth_rw 1 [← add_zero 0, log_mul ha hb]
  exact max_add_add_le_max_add_max

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