English
If a linear operator f on a real or complex inner product space is positive, then its spectrum lies in the nonnegative reals; equivalently, the spectrum is contained in the nonnegative real axis.
Русский
Если линейное отображение f на вещественном или комплексном пространстве с скалярным произведением положительно, то его спектр лежит в неотрицательных вещественных числах.
LaTeX
$$$\sigma(f) \subseteq \mathbb{R}_{\ge 0}$$$
Lean4
theorem spectrumRestricts {f : H →L[𝕜] H} (hf : f.IsPositive) : SpectrumRestricts f ContinuousMap.realToNNReal :=
by
rw [SpectrumRestricts.nnreal_iff]
intro c hc
contrapose! hc
rw [spectrum.notMem_iff, IsUnit.sub_iff, sub_eq_add_neg, ← map_neg]
rw [← neg_pos] at hc
set c := -c
exact
isUnit_of_forall_le_norm_inner_map _ (c := ⟨c, hc.le⟩) hc fun x ↦
calc
‖x‖ ^ 2 * c = re ⟪algebraMap ℝ (H →L[𝕜] H) c x, x⟫_𝕜 := by
rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), coe_smul', Pi.smul_apply,
one_apply, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal, re_ofReal_mul, inner_self_eq_norm_sq,
mul_comm]
_ ≤ re ⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜 := by
simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left] using hf.re_inner_nonneg_left x
_ ≤ ‖⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜‖ := RCLike.re_le_norm _
