norm_commutator_sub_one_le — Mathlib

English

For nonzero a,b, the norm of the commutator a b a^{-1} b^{-1} - 1 is bounded by a specified product involving norms of a,b and their deviations from 1.

Русский

Для ненулевых a,b нормa коммутатора a b a^{-1} b^{-1} - 1 ограничена указанным произведением норм a,b и их отклонений от 1.

LaTeX

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

Lean4

theorem norm_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 norm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

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