pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius

English

Gelfand’s formula asserts that the spectral radius ρ(a) equals the limit of the sequence (‖a^n‖^{1/n}) as n tends to infinity in an appropriate topology, i.e., Tendsto (‖a^n‖^{1/n}) to ρ(a).

Русский

Формула Гельфанда утверждает, что спектральный радиус ρ(a) равен пределу последовательности (‖a^n‖^{1/n}) при n → ∞.

LaTeX

$$$\\displaystyle \\lim_{n\\to\\infty} \\|a^n\\|^{1/n} = \\rho(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_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A) :
    Tendsto (fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) atTop (𝓝 (spectralRadius ℂ a)) :=
  tendsto_of_le_liminf_of_limsup_le (spectralRadius_le_liminf_pow_nnnorm_pow_one_div ℂ a)
    (limsup_pow_nnnorm_pow_one_div_le_spectralRadius a)

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