English
For a unitary element u, every spectral value lies on the unit circle; i.e., spectrum(u) ⊆ {λ ∈ ℂ : |λ| = 1}.
Русский
Для единичного элемента u спектр состоит из точек на единичной окружности; т.е. spectrum(u) ⊆ {λ ∈ ℂ : |λ| = 1}.
LaTeX
$$$$\operatorname{spectrum}_{\mathbb{C}}(u) \subseteq \{\lambda \in \mathbb{C} : |\lambda| = 1\}.$$$$
Lean4
theorem spectrum_subset_circle (u : unitary E) : spectrum 𝕜 (u : E) ⊆ Metric.sphere 0 1 :=
by
nontriviality E
refine fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm ?_ ?_)
· simpa only [CStarRing.norm_coe_unitary u] using norm_le_norm_of_mem hk
· rw [← unitary.val_toUnits_apply u] at hk
have hnk := ne_zero_of_mem_of_unit hk
rw [← inv_inv (unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk
have : ‖k‖⁻¹ ≤ ‖(↑(unitary.toUnits u)⁻¹ : E)‖ := by simpa only [norm_inv] using norm_le_norm_of_mem hk
simpa using inv_le_of_inv_le₀ (norm_pos_iff.mpr hnk) this
