spectralRadius_pow_le — Mathlib

English

For any a and natural n ≠ 0, (spectralRadius a)^n ≤ spectralRadius (a^n).

Русский

Для любого a и натурального n ≠ 0 выполняется (spectralRadius a)^n ≤ spectralRadius (a^n).

LaTeX

$$$\big(\operatorname{spectralRadius}(\mathbb{K}, a)\big)^n \le \operatorname{spectralRadius}(\mathbb{K}, a^n).$$$

Lean4

theorem spectralRadius_pow_le (a : A) (n : ℕ) (hn : n ≠ 0) : (spectralRadius 𝕜 a) ^ n ≤ spectralRadius 𝕜 (a ^ n) :=
  by
  simp only [spectralRadius, ENNReal.iSup₂_pow_of_ne_zero _ hn]
  refine iSup₂_le fun x hx ↦ ?_
  apply le_iSup₂_of_le (x ^ n) (spectrum.pow_mem_pow a n hx)
  simp

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