English
For any a in a complex Banach algebra, the limsup of the sequence (‖a^n‖)^{1/n} is bounded above by the spectral radius ρ(a).
Русский
Для любого a из комплексной банаховой алгебры limsup последовательности (‖a^n‖)^{1/n} не превосходит спектральный радиус ρ(a).
LaTeX
$$$\\displaystyle \\limsup_{n\\to\\infty} \\|a^n\\|^{1/n} \\le \\rho(a)$.$$
Lean4
/-- The `limsup` relationship for the spectral radius used to prove `spectrum.gelfand_formula`. -/
theorem limsup_pow_nnnorm_pow_one_div_le_spectralRadius (a : A) :
limsup (fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) atTop ≤ spectralRadius ℂ a :=
by
refine ENNReal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt fun r r_pos r_lt => ?_)
simp_rw [inv_limsup, ← one_div]
let p : FormalMultilinearSeries ℂ ℂ A := fun n => ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
suffices h : (r : ℝ≥0∞) ≤ p.radius by
convert h
simp only [p, p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]
congr
ext n
rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]
exact fun ha => (lt_self_iff_false _).mp (ha.2.trans_le (one_div_nonneg.mpr n.cast_nonneg : 0 ≤ (1 / n : ℝ)))
have H₁ := (differentiableOn_inverse_one_sub_smul r_lt).hasFPowerSeriesOnBall r_pos
exact ((hasFPowerSeriesOnBall_inverse_one_sub_smul ℂ a).exchange_radius H₁).r_le
