English
For any polynomial p over a seminormed ring R, the spectral value of p is defined as the supremum over all spectralValueTerms(p)(n).
Русский
Для любого полинома p над полем с нормой спектральное значение p задаётся как супремум по n∈ℕ спектральных членов p.
LaTeX
$$$$\operatorname{spectralValue}(p)=\sup_{n\in\mathbb{N}}\operatorname{spectralValueTerms}(p)(n).$$$$
Lean4
/-- The spectral value of a polynomial in `R[X]`, where `R` is a seminormed ring. One motivation
for the spectral value: if the norm on `R` is nonarchimedean, and if a monic polynomial
splits into linear factors, then its spectral value is the norm of its largest root.
See `max_norm_root_eq_spectralValue`. -/
def spectralValue (p : R[X]) : ℝ :=
iSup (spectralValueTerms p)
