English
For a polynomial p, the spectral radius is bounded by the maximum of |p(λ)| over λ ∈ σ(a).
Русский
Для многочлена p спектральный радиус ограничен максимумом |p(λ)| по λ ∈ σ(a).
LaTeX
$$spectralRadius 𝕜 a ≤ max_{λ ∈ σ(a)} |p(λ)| для подходящего polynomial bound$$
Lean4
theorem spectralRadius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) :
spectralRadius 𝕜 a ≤ (‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / (n + 1) : ℝ) * (‖(1 : A)‖₊ : ℝ≥0∞) ^ (1 / (n + 1) : ℝ) :=
by
refine
iSup₂_le fun k hk =>
?_
-- apply easy direction of the spectral mapping theorem for polynomials
have pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1)) := by
simpa only [one_mul, Algebra.algebraMap_eq_smul_one, one_smul, aeval_monomial, one_mul, eval_monomial] using
subset_polynomial_aeval a (@monomial 𝕜 _ (n + 1) (1 : 𝕜))
⟨k, hk, rfl⟩
-- power of the norm is bounded by norm of the power
have nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ ‖a ^ (n + 1)‖₊ * ‖(1 : A)‖₊ := by
simpa only [Real.toNNReal_mul (norm_nonneg _), norm_toNNReal, nnnorm_pow k (n + 1), ENNReal.coe_mul] using
coe_mono
(Real.toNNReal_mono (norm_le_norm_mul_of_mem pow_mem))
-- take (n + 1)ᵗʰ roots and clean up the left-hand side
have hn : 0 < ((n + 1 : ℕ) : ℝ) := mod_cast Nat.succ_pos'
convert monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le using 1
all_goals dsimp
· rw [one_div, pow_rpow_inv_natCast]
positivity
rw [Nat.cast_succ, ENNReal.coe_mul_rpow]
