spectralValueTerms_nonneg — Mathlib

English

For every p and n, spectralValueTerms(p)(n) ≥ 0.

Русский

Для каждого полинома p и индекса n спектральные члены неотрицательны.

LaTeX

$$$$0\le \operatorname{spectralValueTerms}(p)(n)\quad\text{для всех } p,n.$$$$

Lean4

/-- The sequence `spectralValue_terms p` is nonnegative. -/
theorem spectralValueTerms_nonneg (p : R[X]) (n : ℕ) : 0 ≤ spectralValueTerms p n :=
  by
  simp only [spectralValueTerms]
  split_ifs with h
  · exact rpow_nonneg (norm_nonneg _) _
  · exact le_refl _

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