spectralRadius_pow_le' — Mathlib

English

For a and natural n, (spectralRadius a)^n ≤ spectralRadius (a^n) (same as above in HPow form).

Русский

То же неравенство для HPow; (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' [Nontrivial A] (a : A) (n : ℕ) : (spectralRadius 𝕜 a) ^ n ≤ spectralRadius 𝕜 (a ^ n) :=
  by
  cases n
  · simp
  · exact spectralRadius_pow_le a _ (by simp)

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