nnnorm_commutator_sub_one_le — Mathlib

English

The NN-norm analogue: for nonzero a,b, the NN-norm of the commutator a b a^{-1} b^{-1} - 1 is bounded by a similar expression with real NN-norms.

Русский

NN-норма аналогично: для ненулевых a,b NN-нормa коммутатора ограничена аналогичным выражением через NN-нормы.

LaTeX

$$$\|a b a^{-1} b^{-1} - 1\|_+ \\le 2 \|a\|_+^{-1} \|b\|_+^{-1} \|a - 1\|_+ \|b - 1\|_+$$

Lean4

theorem nnnorm_commutator_sub_one_le (ha : a ≠ 0) (hb : b ≠ 0) :
    ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊ := by
  simpa using nnnorm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

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