Hyperbolic operators have Lyapunov forms

In finite dimensions, a bounded operator A on a real inner product space has a Lyapunov form (ContinuousLinearMap.HasLyapunovForm: a symmetric S and c > 0 with c ‖v‖² ≤ ⟪S (A v), v⟫) exactly when A is hyperbolic, that is, when its complexification has no eigenvalue on the imaginary axis. In real terms, there are no ω : ℝ and v, w : E, not both zero, with A v = -ω w and A w = ω v. The forward implication is ContinuousLinearMap.HasLyapunovForm.eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul; this file proves the converse, the existence half of the inertia theorem of Ostrowski and Schneider.

The construction is first carried out over ℂ, by induction on the dimension, along a unitary triangularization. Let u be a unit eigenvector of A, with eigenvalue λ, and let K = u^⊥. In the splitting F = ℂ u ⊕ K, A is block upper triangular,

A (a u + k) = (λ a + ⟪u, A k⟫) u + Q k,

where Q is the compression of A to K. Every eigenvalue of Q is an eigenvalue of A, by ContinuousLinearMap.hasEigenvalue_of_hasEigenvalue_compression_orthogonal_span_singleton, so Q has a Lyapunov form S_K by induction. Then S = re λ • P_u + t • S_K P_K, with P_u and P_K the orthogonal projections, satisfies

re ⟪S (A v), v⟫ ≥ (re λ)² |a|² - |re λ| ‖A‖ |a| ‖k‖ + t c_K ‖k‖²,

and for t large the right side is at least (re λ)² ‖v‖² / 2. Over ℝ, the operator is complexified (ContinuousLinearMap.complexifyL2); the absence of imaginary eigen-pairs says that the complexification has no eigenvalue on the imaginary axis, and the real part of its complex Lyapunov form, restricted to real vectors, is a real Lyapunov form of A.

Combined with TauCeti.WeakDerivStep.isFredholm_trajectoryOperator_of_hasLyapunovForm, this shows that d/ds + A(s) is Fredholm from W^{1,2} to L² for every continuous family A whose limits at ±∞ are hyperbolic.

Main declarations

• ContinuousLinearMap.exists_isSymmetric_forall_mul_norm_sq_le_re_inner_of_re_ne_zero: an operator on a finite-dimensional complex inner product space without eigenvalues on the imaginary axis has a self-adjoint S and c > 0 with c ‖v‖² ≤ re ⟪S (A v), v⟫.
• ContinuousLinearMap.hasLyapunovForm_iff_forall_eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul: on a finite-dimensional real inner product space, A has a Lyapunov form if and only if it has no purely imaginary eigenvalue.

References

• A. Ostrowski and H. Schneider, Some theorems on the inertia of general matrices, J. Math. Anal. Appl. 4 (1962), 72–84.
• R. A. Horn and C. R. Johnson, Topics in Matrix Analysis, Cambridge University Press, 1991, §2.4 (the inertia theorem).

theorem ContinuousLinearMap.exists_isSymmetric_forall_mul_norm_sq_le_re_inner_of_re_ne_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [FiniteDimensional ℂ F] (A : F →L[ℂ] F) (hA : ∀ (μ : ℂ), Module.End.HasEigenvalue (↑A) μ → μ.re ≠ 0) : ∃ (S : F →L[ℂ] F), (↑S).IsSymmetric ∧ ∃ c > 0, ∀ (v : F), c * ‖v‖ ^ 2 ≤ (inner ℂ (S (A v)) v).re

Lyapunov forms over ℂ. If no eigenvalue of an operator A on a finite-dimensional complex inner product space lies on the imaginary axis, then there are a self-adjoint S and c > 0 with c ‖v‖² ≤ re ⟪S (A v), v⟫ for every v.

theorem ContinuousLinearMap.hasLyapunovForm_iff_forall_eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {A : E →L[ℝ] E} : A.HasLyapunovForm ↔ ∀ (ω : ℝ) (v w : E), A v = -ω • w → A w = ω • v → v = 0 ∧ w = 0

Hyperbolic operators have Lyapunov forms. On a finite-dimensional real inner product space, an operator A has a Lyapunov form if and only if it has no purely imaginary eigenvalue: there are no ω and v, w, not both zero, with A v = -ω • w and A w = ω • v. This is the existence half of the inertia theorem of Ostrowski and Schneider.