English
In a normed algebra A, if 1 − z a is invertible whenever the norm of z is small enough relative to the spectral radius of a, then 1 − z a is invertible provided ||z||₊ < 1/ρ(a).
Русский
В нормированной алгебре A элемент 1 − z a оказывается взаимно обратимым, если норма z достаточно мала по отношению к спектральной радиусу a; точнее, при ||z||₊ < 1/ρ(a).
LaTeX
$$$\\|z\\|_{+} < \\rho(a)^{-1} \\quad\\Rightarrow\\quad 1 - z a \\in A^{\\times}$$$
Lean4
theorem isUnit_one_sub_smul_of_lt_inv_radius {a : A} {z : 𝕜} (h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹) :
IsUnit (1 - z • a) := by
by_cases hz : z = 0
· simp only [hz, isUnit_one, sub_zero, zero_smul]
· let u := Units.mk0 z hz
suffices hu : IsUnit (u⁻¹ • (1 : A) - a) by rwa [IsUnit.smul_sub_iff_sub_inv_smul, inv_inv u] at hu
rw [Units.smul_def, ← Algebra.algebraMap_eq_smul_one, ← mem_resolventSet_iff]
refine mem_resolventSet_of_spectralRadius_lt ?_
rwa [Units.val_inv_eq_inv_val, nnnorm_inv, coe_inv (nnnorm_ne_zero_iff.mpr (Units.val_mk0 hz ▸ hz : (u : 𝕜) ≠ 0)),
lt_inv_iff_lt_inv]
