English
Let p be a polynomial over a seminormed ring R. The spectralValueTerms p is the sequence indexed by n in N given by ∥p.coeff n∥^(1/(natDegree(p)−n)) when n is strictly less than natDegree(p), and by 0 otherwise.
Русский
Пусть p — полином над полем, несводимым к нормированному кольцу R. Спектральные_термы p задают последовательность по n∈ℕ: ∥p.coeff n∥^(1/(natDegree(p)−n)) при n < natDegree(p), и 0 в противном случае.
LaTeX
$$$$\operatorname{spectralValueTerms}(p)(n)=\begin{cases} \|p.\coeff(n)\|^{\frac{1}{(p.natDegree-n : \mathbb{R})}} & \text{if } n < p.natDegree \\ 0 & \text{otherwise} \end{cases}$$$$
Lean4
/-- The function `ℕ → ℝ` sending `n` to `‖ p.coeff n ‖^(1/(p.natDegree - n : ℝ))`, if
`n < p.natDegree`, or to `0` otherwise. -/
def spectralValueTerms (p : R[X]) : ℕ → ℝ := fun n : ℕ ↦
if n < p.natDegree then ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) else 0
