Power decay below spectral radius one

In a complex Banach algebra, the powers of an element whose spectral radius is strictly below one converge to zero. This follows from Gelfand's formula spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius: eventually ‖a ^ n‖ ≤ r ^ n for any r strictly between the spectral radius and one.

Main results

• pow_tendsto_zero_of_spectralRadius_lt_one
• geometric_bound_of_spectralRadius_lt_one
• geometric_apply_bound_of_spectralRadius_lt_one
• uniform_eigenvalue_gap_of_finite_lt_one
• uniform_eigenvalue_gap_of_finiteDimensional_lt_one

theorem pow_tendsto_zero_of_spectralRadius_lt_one {A : Type u_1} [NormedRing A] [CompleteSpace A] [NormedAlgebra ℂ A] (a : A) (h : spectralRadius ℂ a < 1) : Filter.Tendsto (fun (n : ℕ) => a ^ n) Filter.atTop (nhds 0)

Powers tend to zero when spectral radius < 1.

theorem geometric_bound_of_spectralRadius_lt_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [CompleteSpace V] (T : V →L[ℂ] V) (hT : spectralRadius ℂ T < 1) : ∃ (C : ℝ) (r : ℝ), 0 < C ∧ 0 < r ∧ r < 1 ∧ ∀ (n : ℕ), ‖T ^ n‖ ≤ C * r ^ n

Gelfand's formula: if spectralRadius(T) < 1, then ‖T ^ n‖ ≤ C · r ^ n for some C > 0 and 0 < r < 1, uniformly in n.

theorem geometric_apply_bound_of_spectralRadius_lt_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [CompleteSpace V] (T : V →L[ℂ] V) (hT : spectralRadius ℂ T < 1) : ∃ (C : ℝ) (r : ℝ), 0 < C ∧ 0 < r ∧ r < 1 ∧ ∀ (n : ℕ) (x : V), ‖(T ^ n) x‖ ≤ C * r ^ n * ‖x‖

If spectralRadius(T) < 1, then the powers of T satisfy the pointwise bound ‖T ^ n x‖ ≤ C · r ^ n · ‖x‖ for some C > 0 and 0 < r < 1.

Uniform eigenvalue gaps

theorem uniform_eigenvalue_gap_of_finite_lt_one {K : Type u_1} {V : Type u_2} [NormedField K] [AddCommGroup V] [Module K V] {E : V →ₗ[K] V} (hfin : {μ : K | Module.End.HasEigenvalue E μ}.Finite) (hlt : ∀ (μ : K), Module.End.HasEigenvalue E μ → μ ≠ 1 → ‖μ‖ < 1) : ∃ δ > 0, ∀ (μ : K), Module.End.HasEigenvalue E μ → μ ≠ 1 → ‖μ‖ ≤ 1 - δ

Uniform eigenvalue gap from finitely many eigenvalues with modulus below one.

If an endomorphism has finitely many eigenvalues, and every eigenvalue μ ≠ 1 satisfies ‖μ‖ < 1, then there is a uniform δ > 0 such that ‖μ‖ ≤ 1 - δ for every non-unit eigenvalue.

theorem uniform_eigenvalue_gap_of_finiteDimensional_lt_one {K : Type u_1} {V : Type u_2} [NormedField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {E : V →ₗ[K] V} (hlt : ∀ (μ : K), Module.End.HasEigenvalue E μ → μ ≠ 1 → ‖μ‖ < 1) : ∃ δ > 0, ∀ (μ : K), Module.End.HasEigenvalue E μ → μ ≠ 1 → ‖μ‖ ≤ 1 - δ

A finite-dimensional endomorphism whose non-unit eigenvalues have modulus below one has a uniform eigenvalue gap.