English
Spectral radius is bounded by liminf of powers of the norm: spectralRadius 𝕜 a ≤ liminf_{n→∞} (‖a^n‖₊)^{1/n}.
Русский
Спектральный радиус ограничен liminf последовательности (‖a^n‖₊)^{1/n}.
LaTeX
$$spectralRadius 𝕜 a ≤ \\liminf_{n→∞} (\\|a^n\\|_{+})^{1/n}$$
Lean4
theorem spectralRadius_le_liminf_pow_nnnorm_pow_one_div (a : A) :
spectralRadius 𝕜 a ≤ atTop.liminf fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) :=
by
refine ENNReal.le_of_forall_lt_one_mul_le fun ε hε => ?_
by_cases h : ε = 0
· simp only [h, zero_mul, zero_le']
simp only [ENNReal.mul_le_iff_le_inv h (hε.trans_le le_top).ne, mul_comm ε⁻¹, liminf_eq_iSup_iInf_of_nat',
ENNReal.iSup_mul]
conv_rhs => arg 1; intro i; rw [ENNReal.iInf_mul (by simp [h])]
rw [← ENNReal.inv_lt_inv, inv_one] at hε
obtain ⟨N, hN⟩ := eventually_atTop.mp (ENNReal.eventually_pow_one_div_le (ENNReal.coe_ne_top : ↑‖(1 : A)‖₊ ≠ ∞) hε)
refine le_trans ?_ (le_iSup _ (N + 1))
refine le_iInf fun n => ?_
simp only [← add_assoc]
refine (spectralRadius_le_pow_nnnorm_pow_one_div 𝕜 a (n + N)).trans ?_
norm_cast
exact mul_le_mul_left' (hN (n + N + 1) (by cutsat)) _
