English
If p is monic, then spectralValue(p) = 0 iff p = X^{natDegree(p)}.
Русский
Пусть p моноидальный. Тогда spectralValue(p) = 0 тогда и только тогда, когда p = X^{natDegree(p)}.
LaTeX
$$$$\operatorname{spectralValue}(p) = 0 \;\Leftrightarrow\; p = X^{\,p.natDegree}.$$$$
Lean4
/-- The spectral value of `p` equals zero if and only if `p` is of the form `X ^ n`. -/
theorem spectralValue_eq_zero_iff [Nontrivial R] {p : R[X]} (hp : p.Monic) :
spectralValue p = 0 ↔ p = X ^ p.natDegree :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ spectralValue_X_pow p.natDegree⟩
rw [spectralValue] at h
ext n
rw [coeff_X_pow]
split_ifs with hn
· rw [hn, coeff_natDegree]; exact hp
· by_cases hn' : n < p.natDegree
· have h_le : iSup (spectralValueTerms p) ≤ 0 := h.le
have h_exp : 0 < 1 / ((p.natDegree : ℝ) - n) :=
by
rw [one_div_pos, ← cast_sub (le_of_lt hn'), cast_pos]
exact Nat.sub_pos_of_lt hn'
have h0 : (0 : ℝ) = 0 ^ (1 / ((p.natDegree : ℝ) - n)) := by rw [zero_rpow (ne_of_gt h_exp)]
rw [iSup, csSup_le_iff (spectralValueTerms_bddAbove p) (Set.range_nonempty _)] at h_le
specialize h_le (spectralValueTerms p n) ⟨n, rfl⟩
simp only [spectralValueTerms, if_pos hn'] at h_le
rw [h0, rpow_le_rpow_iff (norm_nonneg _) (le_refl _) h_exp] at h_le
exact norm_eq_zero.mp (le_antisymm h_le (norm_nonneg _))
· exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne (le_of_not_gt hn') (ne_comm.mpr hn))
