English
If the spectrum σ𝕜(a) is nonempty, there exists k ∈ σ𝕜(a) such that (‖k‖₊) equals the spectral radius of a.
Русский
Если спектр σ𝕜(a) непуст, существует k ∈ σ𝕜(a) такой, что ‖k‖₊ равно спектральному радиусу a.
LaTeX
$$If (σ 𝕜(a)).Nonempty, then ∃ k ∈ σ 𝕜(a), (‖k‖₊) = spectralRadius 𝕜 a.$$
Lean4
theorem resolvent_isBigO_inv (a : A) : resolvent a =O[cobounded 𝕜] Inv.inv :=
have h : (fun z ↦ resolvent (z⁻¹ • a) (1 : 𝕜)) =O[cobounded 𝕜] (fun _ ↦ (1 : ℝ)) := by
simpa [Function.comp_def, resolvent] using
(NormedRing.inverse_one_sub_norm (R := A)).comp_tendsto
(by simpa using (tendsto_inv₀_cobounded (α := 𝕜)).smul_const a)
calc
resolvent a =ᶠ[cobounded 𝕜] fun z ↦ z⁻¹ • resolvent (z⁻¹ • a) (1 : 𝕜) :=
by
filter_upwards [isBounded_singleton (x := 0)] with z hz
lift z to 𝕜ˣ using Ne.isUnit hz
simpa [Units.smul_def] using congr(z⁻¹ • $(units_smul_resolvent_self (r := z) (a := a)))
_ =O[cobounded 𝕜] (·⁻¹) := .of_norm_right <| by simpa using (isBigO_refl (·⁻¹) (cobounded 𝕜)).norm_right.smul h
