English
For units a, b in a normed ring, the commutator a b a^{-1} b^{-1} is close to 1: the distance to 1 is bounded by a product of norms of a^{-1}, b^{-1}, a−1, b−1 and a−1 minus 1, with a universal constant 2.
Русский
Для единиц a, b в нормированном кольце расстояние до 1 для коммутатора a b a^{-1} b^{-1} ограничено произведением норм a^{-1}, b^{-1}, a−1, b−1 и a−1 − 1, b−1 − 1, умноженным на 2.
LaTeX
$$$\|a b a^{-1} b^{-1} - 1\| ≤ 2 \|a^{-1}\| \|b^{-1}\| \|a - 1\| \|b - 1\|$$$
Lean4
theorem norm_commutator_units_sub_one_le (a b : αˣ) :
‖(a * b * a⁻¹ * b⁻¹).val - 1‖ ≤ 2 * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ * ‖a.val - 1‖ * ‖b.val - 1‖ :=
calc
‖(a * b * a⁻¹ * b⁻¹).val - 1‖ = ‖(a * b - b * a) * a⁻¹.val * b⁻¹.val‖ := by simp [sub_mul, *]
_ ≤ ‖(a * b - b * a : α)‖ * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ := norm_mul₃_le
_ = ‖(a - 1 : α) * (b - 1) - (b - 1) * (a - 1)‖ * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ := by simp_rw [sub_one_mul, mul_sub_one];
abel_nf
_ ≤ (‖(a - 1 : α) * (b - 1)‖ + ‖(b - 1 : α) * (a - 1)‖) * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ := by gcongr; exact norm_sub_le ..
_ ≤ (‖a.val - 1‖ * ‖b.val - 1‖ + ‖b.val - 1‖ * ‖a.val - 1‖) * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ := by
gcongr <;> exact norm_mul_le ..
_ = 2 * ‖a⁻¹.val‖ * ‖b⁻¹.val‖ * ‖a.val - 1‖ * ‖b.val - 1‖ := by ring
