English
For a self-adjoint a, every z ∈ spectrum( a ) is real; equivalently spectrum(a) ⊆ ℝ.
Русский
Для сам-сопряженного a каждый z в спектре a реален; спектр лежит в ℝ.
LaTeX
$$$$\forall z \in \operatorname{spectrum}_{\mathbb{C}}(a),\ z \in \mathbb{R}.$$$$
Lean4
/-- Any element of the spectrum of a selfadjoint is real. -/
theorem mem_spectrum_eq_re {a : A} (ha : IsSelfAdjoint a) {z : ℂ} (hz : z ∈ spectrum ℂ a) : z = z.re :=
by
have hu := exp_mem_unitary_of_mem_skewAdjoint ℂ (ha.smul_mem_skewAdjoint conj_I)
let Iu := Units.mk0 I I_ne_zero
have : NormedSpace.exp ℂ (I • z) ∈ spectrum ℂ (NormedSpace.exp ℂ (I • a)) := by
simpa only [Units.smul_def, Units.val_mk0] using spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
exact
Complex.ext (ofReal_re _) <| by
simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff, smul_eq_mul, I_mul,
neg_eq_zero] using spectrum.subset_circle_of_unitary hu this
