spectralNorm — Mathlib

English

spectralValue(p) is defined as the supremum of spectralValueTerms(p).

Русский

spectralValue(p) задаётся как супремум spectralValueTerms(p).

LaTeX

$$$$\operatorname{spectralValue}(p)=\iSup_{n\in\mathbb{N}}\operatorname{spectralValueTerms}(p)(n).$$$$

Lean4

/-- If `L` is an algebraic extension of a normed field `K` and `y : L` then the spectral norm
  `spectralNorm K y : ℝ` of `y` (written `|y|_sp` in the textbooks) is the spectral value of the
  minimal polynomial of `y` over `K`. -/
def spectralNorm (y : L) : ℝ :=
  spectralValue (minpoly K y)

Похожие утверждения