posLog_add — Mathlib

English

For real numbers a and b: log⁺(a + b) ≤ log 2 + log⁺ a + log⁺ b.

Русский

Для действительных a и b: log⁺(a + b) ≤ log 2 + log⁺ a + log⁺ b.

LaTeX

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

Lean4

/-- Estimate for `log⁺` of a sum. See `Real.posLog_sum` for a variant involving
multiple summands. -/
theorem posLog_add {a b : ℝ} : log⁺ (a + b) ≤ log 2 + log⁺ a + log⁺ b := by
  convert posLog_sum Finset.univ ![a, b] using 1 <;> simp [add_assoc]

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