English
For a NormedAddCommGroup E and a,b ∈ E: log⁺(‖a + b‖) ≤ log⁺(‖a‖) + log⁺(‖b‖) + log 2.
Русский
Для нормированной аддитивной коммутативной группы E и элементов a, b: log⁺(‖a + b‖) ≤ log⁺(‖a‖) + log⁺(‖b‖) + log 2.
LaTeX
$$$\log^{+}\|a + b\| \le \log^{+}\|a\| + \log^{+}\|b\| + \log 2$$$
Lean4
/-- Variant of `posLog_add` for norms of elements in normed additive commutative groups, using
monotonicity of `log⁺` and the triangle inequality.
-/
theorem posLog_norm_add_le {E : Type*} [NormedAddCommGroup E] (a b : E) : log⁺ ‖a + b‖ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 :=
by
calc
log⁺ ‖a + b‖
_ ≤ log⁺ (‖a‖ + ‖b‖) := by
apply monotoneOn_posLog _ _ (norm_add_le a b) <;> simp [add_nonneg (norm_nonneg a) (norm_nonneg b)]
_ ≤ log⁺ ‖a‖ + log⁺ ‖b‖ + log 2 := by
convert posLog_add using 1
ring
