Lyapunov forms of bounded operators

A bounded operator A on a real inner product space has a Lyapunov form if there are a symmetric operator S and a constant c > 0 with

c ‖v‖² ≤ ⟪S (A v), v⟫ for every v.

For matrices this is the Lyapunov inequality S A + Aᵀ S ≥ 2c > 0. The quadratic form q(v) = ⟪S v, v⟫ then decreases at rate at least 2c ‖v‖² along every solution of v' = -A v, and this monotonicity is what turns the condition into coercive estimates for the first-order operator d/ds + A on the line. No symmetry of A is required, and S may be indefinite. A symmetric operator with α ‖v‖ ≤ ‖A v‖ has the Lyapunov form S = A with c = α².

In finite dimensions, the inertia theorem of Ostrowski and Schneider identifies the operators with a Lyapunov form as the hyperbolic ones, those without eigenvalues on the imaginary axis. This file proves the easy half: an operator with a Lyapunov form has no purely imaginary eigenvalue (ContinuousLinearMap.HasLyapunovForm.eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul). The converse is ContinuousLinearMap.hasLyapunovForm_iff_forall_eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul in TauCeti.Analysis.InnerProductSpace.LyapunovForm.Hyperbolic.

Main declarations

• ContinuousLinearMap.HasLyapunovForm: A has a Lyapunov form, unfolded by ContinuousLinearMap.hasLyapunovForm_iff.
• ContinuousLinearMap.isSymmetric_neg_and_forall_le_inner_neg_apply_neg_apply: -S is a Lyapunov form of -A whenever S is one of A, with the same constant; ContinuousLinearMap.HasLyapunovForm.neg is the corresponding statement for HasLyapunovForm.
• ContinuousLinearMap.hasLyapunovForm_of_isSymmetric: a symmetric operator bounded below has a Lyapunov form; ContinuousLinearMap.hasLyapunovForm_of_tendsto_of_isSymmetric applies this to a limit of symmetric operators, and ContinuousLinearMap.hasLyapunovForm_sub_smul_id_of_isSymmetric to its shifts A - c • id with |c| below the bound.
• ContinuousLinearMap.HasLyapunovForm.exists_eventually_nhds: one Lyapunov form serves every operator close enough to A; ContinuousLinearMap.isOpen_setOf_hasLyapunovForm is the corresponding openness statement.
• ContinuousLinearMap.mul_norm_le_opNorm_mul_norm_apply_of_forall_le_inner: a symmetric Lyapunov form S of A satisfies c ‖v‖ ≤ ‖A‖ ‖S v‖, so it is bounded below (ContinuousLinearMap.exists_pos_forall_mul_norm_le_norm_apply_of_forall_le_inner).
• ContinuousLinearMap.hasLyapunovForm_one_sub_smul_add_smul: a symmetric Lyapunov form S of A is a Lyapunov form of every (1 - t) A + t S with 0 ≤ t ≤ 1, which joins A to the bounded-below symmetric operator S through operators with Lyapunov forms.
• ContinuousLinearMap.HasLyapunovForm.eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul: A has no purely imaginary eigenvalue, and in particular is injective.
• ContinuousLinearMap.HasLyapunovForm.neg_adjoint: in finite dimensions, -A† has a Lyapunov form whenever A does. The formal adjoint of d/ds + A is -d/ds + A†; multiplying it by -1 gives d/ds - A†, whose coefficient is -A†.

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).

def ContinuousLinearMap.HasLyapunovForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →L[ℝ] E) : Prop

A bounded operator A has a Lyapunov form if there are a symmetric operator S and a constant c > 0 with c ‖v‖² ≤ ⟪S (A v), v⟫ for every v: the matrix inequality S A + Aᵀ S ≥ 2c. In finite dimensions this characterizes hyperbolic operators.

theorem ContinuousLinearMap.hasLyapunovForm_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} : A.HasLyapunovForm ↔ ∃ (S : E →L[ℝ] E), (↑S).IsSymmetric ∧ ∃ c > 0, ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ (S (A v)) v

Unfolding ContinuousLinearMap.HasLyapunovForm.

theorem ContinuousLinearMap.isSymmetric_neg_and_forall_le_inner_neg_apply_neg_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A S : E →L[ℝ] E} {c : ℝ} (hS : (↑S).IsSymmetric) (hcS : ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ (S (A v)) v) : (↑(-S)).IsSymmetric ∧ ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ ((-S) ((-A) v)) v

Negating a Lyapunov form. If S is a Lyapunov form of A with constant c, then -S is one of -A with the same constant. Along the flow of A this reverses time.

theorem ContinuousLinearMap.HasLyapunovForm.neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} (h : A.HasLyapunovForm) : (-A).HasLyapunovForm

If A has a Lyapunov form, then so does -A.

theorem ContinuousLinearMap.hasLyapunovForm_of_isSymmetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} (hA : (↑A).IsSymmetric) {α : ℝ} (hα : 0 < α) (hgap : ∀ (v : E), α * ‖v‖ ≤ ‖A v‖) : A.HasLyapunovForm

A symmetric operator bounded below has a Lyapunov form, namely S = A with c = α².

theorem ContinuousLinearMap.hasLyapunovForm_of_tendsto_of_isSymmetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → E →L[ℝ] E} (hF : ∀ (i : ι), (↑(F i)).IsSymmetric) (hlim : Filter.Tendsto F l (nhds A)) {α : ℝ} (hα : 0 < α) (hgap : ∀ (v : E), α * ‖v‖ ≤ ‖A v‖) : A.HasLyapunovForm

A limit of symmetric operators bounded below has a Lyapunov form. If symmetric operators F i tend to A and α ‖v‖ ≤ ‖A v‖ with α > 0, then A is symmetric, so it has the Lyapunov form S = A.

theorem ContinuousLinearMap.hasLyapunovForm_sub_smul_id_of_isSymmetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} (hA : (↑A).IsSymmetric) {α c : ℝ} (hgap : ∀ (v : E), α * ‖v‖ ≤ ‖A v‖) (hc : |c| < α) : (A - c • ContinuousLinearMap.id ℝ E).HasLyapunovForm

A symmetric operator bounded below keeps a Lyapunov form under small shifts. If A is symmetric with α ‖v‖ ≤ ‖A v‖ and |c| < α, then A - c • id is symmetric with (α - |c|) ‖v‖ ≤ ‖(A - c • id) v‖, so it has a Lyapunov form.

theorem ContinuousLinearMap.HasLyapunovForm.exists_eventually_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} (h : A.HasLyapunovForm) : ∃ (S : E →L[ℝ] E), (↑S).IsSymmetric ∧ ∃ c > 0, ∀ᶠ (B : E →L[ℝ] E) in nhds A, ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ (S (B v)) v

A Lyapunov form survives small perturbations. If A has a Lyapunov form, then a single symmetric S and a single constant c > 0 satisfy c ‖v‖² ≤ ⟪S (B v), v⟫ for every B close enough to A.

theorem ContinuousLinearMap.isOpen_setOf_hasLyapunovForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsOpen {A : E →L[ℝ] E | A.HasLyapunovForm}

The operators with a Lyapunov form are an open set.

theorem ContinuousLinearMap.HasLyapunovForm.eq_zero_of_apply_eq_neg_smul_of_apply_eq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} (h : A.HasLyapunovForm) {ω : ℝ} {v w : E} (hv : A v = -ω • w) (hw : A w = ω • v) : v = 0 ∧ w = 0

An operator with a Lyapunov form has no purely imaginary eigenvalue. If A v = -ω • w and A w = ω • v, so that v + i w is an eigenvector of the complexification of A with eigenvalue i ω, then v = 0 and w = 0.

theorem ContinuousLinearMap.mul_norm_le_opNorm_mul_norm_apply_of_forall_le_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A S : E →L[ℝ] E} (hS : (↑S).IsSymmetric) {c : ℝ} (h : ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ (S (A v)) v) (v : E) : c * ‖v‖ ≤ ‖A‖ * ‖S v‖

The norm estimate for a Lyapunov form. If S is symmetric and c ‖v‖² ≤ ⟪S (A v), v⟫ for every v, then c ‖v‖ ≤ ‖A‖ ‖S v‖.

theorem ContinuousLinearMap.exists_pos_forall_mul_norm_le_norm_apply_of_forall_le_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A S : E →L[ℝ] E} (hS : (↑S).IsSymmetric) {c : ℝ} (hc : 0 < c) (h : ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ (S (A v)) v) : ∃ α > 0, ∀ (v : E), α * ‖v‖ ≤ ‖S v‖

A symmetric Lyapunov form S of A, with c ‖v‖² ≤ ⟪S (A v), v⟫ and c > 0, is bounded below by a positive constant: α ‖v‖ ≤ ‖S v‖.

theorem ContinuousLinearMap.hasLyapunovForm_one_sub_smul_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A S : E →L[ℝ] E} (hS : (↑S).IsSymmetric) {c : ℝ} (hc : 0 < c) (h : ∀ (v : E), c * ‖v‖ ^ 2 ≤ inner ℝ (S (A v)) v) {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : ((1 - t) • A + t • S).HasLyapunovForm

A Lyapunov form is a Lyapunov form along the segment to itself. If S is a symmetric Lyapunov form of A, with c ‖v‖² ≤ ⟪S (A v), v⟫ and c > 0, then for 0 ≤ t ≤ 1 the operator (1 - t) A + t S has the Lyapunov form S, since ⟪S (S v), v⟫ = ‖S v‖². So every operator with a symmetric Lyapunov form is joined to a bounded-below symmetric operator through operators with Lyapunov forms.

theorem ContinuousLinearMap.HasLyapunovForm.injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} (h : A.HasLyapunovForm) : Function.Injective ⇑A

An operator with a Lyapunov form is injective.

theorem ContinuousLinearMap.HasLyapunovForm.neg_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →L[ℝ] E} [FiniteDimensional ℝ E] (h : A.HasLyapunovForm) : (-adjoint A).HasLyapunovForm

The negated adjoint has a Lyapunov form. In finite dimensions, if A has the Lyapunov form S, then -A† has the Lyapunov form -S⁻¹. The operator -A† is the coefficient of d/ds - A†, the negative of the formal adjoint -d/ds + A† of d/ds + A.