spectralRadius_lt_of_forall_lt_of_nonempty

English

If (σ a) is nonempty and every spectral value is less than r, then spectralRadius 𝕜 a < r.

Русский

Если спектр непуст и все значения спектра меньше r, то спектральный радиус меньше r.

LaTeX

$$$\\text{If } (\\sigma a).Nonempty \\text{ and } (\\forall k \\in \\sigma a, \\|k\\|₊ < r), \\; \\text{ then } \\mathrm{spectralRadius}(\\mathbb{K}, a) < r.$$$

Lean4

theorem spectralRadius_lt_of_forall_lt_of_nonempty [ProperSpace 𝕜] {a : A} (ha : (σ a).Nonempty) {r : ℝ≥0}
    (hr : ∀ k ∈ σ a, ‖k‖₊ < r) : spectralRadius 𝕜 a < r :=
  sSup_image.symm.trans_lt <|
    ((spectrum.isCompact a).sSup_lt_iff_of_continuous ha continuous_enorm.continuousOn (r : ℝ≥0∞)).mpr
      (by simpa using hr)

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