English
The NNReal spectral radius of a is realized inside the spectrum of a in the real setting and maps to spectrum membership.
Русский
NNReal-спектральная радиусa реализуется внутри спектра a в реальном контексте и включается в спектр.
LaTeX
$$spectralRadius Real a.toNNReal ∈ spectrum ℝ a$$
Lean4
theorem nnreal_iff_spectralRadius_le [Algebra ℝ A] {a : A} {t : ℝ≥0} (ht : spectralRadius ℝ a ≤ t) :
SpectrumRestricts a ContinuousMap.realToNNReal ↔ spectralRadius ℝ (algebraMap ℝ A t - a) ≤ t :=
by
have : spectrum ℝ a ⊆ Set.Icc (-t) t := by
intro x hx
rw [Set.mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe, ← ENNReal.coe_le_coe]
exact le_iSup₂ (α := ℝ≥0∞) x hx |>.trans ht
rw [nnreal_iff]
refine ⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩
· rw [← spectrum.singleton_sub_eq] at hx
obtain ⟨y, hy, rfl⟩ : ∃ y ∈ spectrum ℝ a, ↑t - y = x := by simpa using hx
obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy
lift y to ℝ≥0 using h y hy
rw [← NNReal.coe_sub (by exact_mod_cast hyt)]
simp
· replace h : ∀ x ∈ spectrum ℝ a, ‖t - x‖₊ ≤ t := by
simpa [spectralRadius, iSup₂_le_iff, ← spectrum.singleton_sub_eq] using h
peel h with x hx h_le
rw [← NNReal.coe_le_coe, coe_nnnorm, Real.norm_eq_abs, abs_le] at h_le
linarith [h_le.2]
