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
• geometric_apply_bound_of_spectralRadius_lt
• geometric_bound_of_spectralRadius_lt_one
• geometric_apply_bound_of_spectralRadius_lt_one
• spectralRadius_lt_one_of_eigenvalues_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 {A : Type u_1} [NormedRing A] [CompleteSpace A] [NormedAlgebra ℂ A] (a : A) (rate : NNReal) (ha : spectralRadius ℂ a < ↑rate) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), ‖a ^ n‖ ≤ C * ↑rate ^ n

If the spectral radius of an element of a complex Banach algebra is strictly smaller than a prescribed rate $\lambda$, then its powers satisfy $\lVert a^n\rVert \le C\lambda^n$ for every $n$. The constant $C>0$ may depend on the prescribed rate $\lambda$.

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

If the spectral radius of a continuous linear endomorphism is strictly smaller than a prescribed rate $\lambda$, then $\lVert T^n x\rVert \le C\lambda^n\lVert x\rVert$ for every $n$ and $x$. The constant $C>0$ may depend on the prescribed rate $\lambda$.

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.

theorem spectralRadius_lt_one_of_eigenvalues_lt_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] [Nontrivial V] (F : V →ₗ[ℂ] V) (hF : ∀ (ν : ℂ), Module.End.HasEigenvalue F ν → ‖ν‖ < 1) : spectralRadius ℂ ((Module.End.toContinuousLinearMap V) F) < 1

In a nontrivial finite-dimensional complex normed space, a strict modulus bound on all eigenvalues of an endomorphism gives a spectral-radius gap.

The result follows from Mathlib's spectral-radius bound because, over $\mathbb C$, the spectrum of a finite-dimensional endomorphism is exactly its set of eigenvalues.

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.