spectralValueTerms_of_lt_natDegree

English

If n is less than the degree of p, the nth spectralValueTerm is the nth coefficient’s norm raised to the reciprocal of the remaining degree gap.

Русский

Если n < deg(p), то n-й спектральный член равен норме коэффициента при n, возведённой в обратную дробь степени, недостающей до natDegree.

LaTeX

$$$$\operatorname{spectralValueTerms}(p)(n)=\|p.\coeff(n)\|^{\frac{1}{(p.natDegree-n : \mathbb{R})}}\quad\text{при } n

Lean4

theorem spectralValueTerms_of_lt_natDegree (p : R[X]) {n : ℕ} (hn : n < p.natDegree) :
    spectralValueTerms p n = ‖p.coeff n‖ ^ (1 / (p.natDegree - n : ℝ)) := by simp [spectralValueTerms, if_pos hn]

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