pow_norm_pow_one_div_tendsto_nhds_spectralRadius

English

In a complex Banach algebra, the spectral radius is the limit of the sequence (‖a^n‖)^{1/n} (or its ENNReal version) as n → ∞.

Русский

В комплексной банаховой алгебре спектральный радиус является пределом последовательности (‖a^n‖)^{1/n} (или его версии ENNReal) при n → ∞.

LaTeX

$$$\\displaystyle \\lim_{n\\to\\infty} \\mathrm{ENNReal\\,ofReal} (\\|a^n\\|^{1/n}) = \\rho_\\mathbb{C}(a)$$$

Lean4

/-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖₊ ^ (1 / n)`. -/
theorem pow_norm_pow_one_div_tendsto_nhds_spectralRadius (a : A) :
    Tendsto (fun n : ℕ => ENNReal.ofReal (‖a ^ n‖ ^ (1 / n : ℝ))) atTop (𝓝 (spectralRadius ℂ a)) :=
  by
  convert pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a using 1
  ext1
  rw [← ofReal_rpow_of_nonneg (norm_nonneg _) _, ← coe_nnnorm, coe_nnreal_eq]
  exact one_div_nonneg.mpr (mod_cast zero_le _)

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