English
For a real Banach algebra A and a ∈ A with nonempty spectrum, the real part of the spectral radius belongs to the spectrum of a real-valued embedding.
Русский
Для действительной банаховой алгебры A и элемента a с ненулевым спектром, соответствующая вещественная спектральная величина принадлежит спектру a при отображении в Real.
LaTeX
$$spectralRadius Real a ∈ spectrum Real a$$
Lean4
/-- If `𝕜₁` is a normed field contained as subfield of a larger normed field `𝕜₂`, and if `a : A`
is an element whose `𝕜₂` spectrum restricts to `𝕜₁`, then the spectral radii over each scalar
field coincide. -/
theorem spectralRadius_eq {𝕜₁ 𝕜₂ A : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedRing A] [NormedAlgebra 𝕜₁ A]
[NormedAlgebra 𝕜₂ A] [NormedAlgebra 𝕜₁ 𝕜₂] [IsScalarTower 𝕜₁ 𝕜₂ A] {f : 𝕜₂ → 𝕜₁} {a : A}
(h : SpectrumRestricts a f) : spectralRadius 𝕜₁ a = spectralRadius 𝕜₂ a :=
by
rw [spectralRadius, spectralRadius]
have := algebraMap_isometry 𝕜₁ 𝕜₂ |>.nnnorm_map_of_map_zero (map_zero _)
apply le_antisymm
all_goals apply iSup₂_le fun x hx ↦ ?_
· refine congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_
exact (spectrum.algebraMap_mem_iff _).mpr hx
· have ⟨y, hy, hy'⟩ := h.algebraMap_image.symm ▸ hx
subst hy'
exact this y ▸ le_iSup₂ (α := ℝ≥0∞) y hy
