spectralRadius_lt_of_forall_lt — Mathlib

English

The spectral mapping theorem for polynomials in a complex Banach algebra: spectrum of aeval(a, p) equals the image under eval of the spectrum of a.

Русский

Спектральное отображение полиномов в комплексной банаховой алгебре: спектр $\\text{aeval}(a,p)$ равен образу спектра $a$ под отображением $p$.

LaTeX

$$$\\mathrm{spec}_{\\mathbb{C}}(\\mathrm{aeval}(a,p)) = \\{ \\mathrm{eval}_k(p) : k \\in \\mathrm{spec}_{\\mathbb{C}}(a) \\}$$$

Lean4

/-- In a complex Banach algebra, if every element of the spectrum has norm strictly less than
`r : ℝ≥0`, then the spectral radius is also strictly less than `r`. -/
theorem spectralRadius_lt_of_forall_lt (a : A) {r : ℝ≥0} (hr : ∀ z ∈ spectrum ℂ a, ‖z‖₊ < r) : spectralRadius ℂ a < r :=
  spectralRadius_lt_of_forall_lt_of_nonempty (spectrum.nonempty a) hr

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