spectralRadius_mem_spectrum_or — Mathlib

English

Either the real spectral radius lies in the spectrum or its negative lies in the spectrum.

Русский

Либо вещественный спектр входит в спектр, либо его отрицание входит в спектр.

LaTeX

$$Real.spectralRadius_mem_spectrum_or ha$$

Lean4

theorem _root_.Real.spectralRadius_mem_spectrum_or {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
    {a : A} (ha : (spectrum ℝ a).Nonempty) :
    (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a :=
  by
  obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha
  simp only [← hx₂, ENNReal.coe_toReal, coe_nnnorm, Real.norm_eq_abs]
  exact abs_choice x |>.imp (fun h ↦ by rwa [h]) (fun h ↦ by simpa [h])

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