English
Let μ be a real eigenvalue of T with eigenvector v. If for all x the real part of ⟨x, Tx⟩ is strictly positive, then μ is strictly positive.
Русский
Пусть μ — вещественное собственное значение T с собственным вектором v. Если для всех x выполняется строго положительная часть ⟨x, Tx⟩, то μ > 0.
LaTeX
$$$0 < \mu$$$
Lean4
theorem eigenvalue_pos_of_pos {μ : ℝ} {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_pos_iff_of_pos_right hpos).mp (this ▸ hnn v)
