English
Let μ be a real eigenvalue of a linear operator T on an inner product space E. If for every x the real part of ⟨x, Tx⟩ is nonnegative, then μ is nonnegative.
Русский
Пусть μ — вещественное собственное значение линейного отображения T на пространстве E с скалярным произведением. Если для всех x выполняется положительная часть ⟨x, Tx⟩, то μ неотрицательно.
LaTeX
$$$0 \le \mu$$$
Lean4
theorem eigenvalue_nonneg_of_nonneg {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : HasEigenvalue T μ)
(hnn : ∀ x : E, 0 ≤ RCLike.re ⟪x, T x⟫) : 0 ≤ μ :=
by
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂
simp only [mem_genEigenspace_one] at hv₁
have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 := mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)
exact (mul_nonneg_iff_of_pos_right hpos).mp (this ▸ hnn v)
