Exponential dichotomy for symmetric linear flows

A finite-dimensional symmetric operator has negative and positive spectral subspaces. For the flow generated by its negative, a vector of the positive subspace has norm at most exp (-α t) * ‖v‖ in forward time, and a vector of the negative subspace has norm at most exp (α t) * ‖v‖ in backward time, where α is any lower bound on the relevant absolute eigenvalues. These bounds decay — that is, they are genuine contractions — exactly when α is positive, and since the nonzero spectrum is finite one common positive rate always exists. When the kernel is zero, the two subspaces are complementary and these estimates form an exponential dichotomy.

These estimates are the quantitative counterpart of the asymptotic description in TauCeti.Analysis.ODE.Linear. They are the linear input to the Lyapunov--Perron construction of local stable and unstable manifolds near a hyperbolic equilibrium.

Main declarations

• LinearMap.IsSymmetric.norm_flow_neg_le_exp_neg_mul_of_mem_positiveSpectralSubspace: the forward exponential norm bound on the positive spectral subspace.
• LinearMap.IsSymmetric.norm_flow_neg_le_exp_mul_of_mem_negativeSpectralSubspace: the backward exponential norm bound on the negative spectral subspace.
• LinearMap.IsSymmetric.exists_exponential_bounds_spectralSubspaces: a symmetric operator has a common positive contraction rate on its two strict spectral subspaces.
• ContinuousLinearMap.IsIdempotentElem.exists_projection_exponential_bounds: exponential bounds on the range and kernel of an idempotent operator give bounds in projection form.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

theorem LinearMap.IsSymmetric.norm_flow_neg_le_exp_neg_mul_of_mem_positiveSpectralSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →L[ℝ] E} (hT : (↑T).IsSymmetric) (hn : Module.finrank ℝ E = n) {alpha t : ℝ} (halpha : ∀ (i : Fin n), 0 < hT.eigenvalues hn i → alpha ≤ hT.eigenvalues hn i) (ht : 0 ≤ t) {v : E} (hv : v ∈ hT.positiveSpectralSubspace hn) : ‖(-T).flow.toFun t v‖ ≤ Real.exp (-alpha * t) * ‖v‖

For the flow generated by -T, a vector of the positive spectral subspace has norm at most exp (-α t) * ‖v‖ in forward time, for any α below all the positive eigenvalues. The bound decays exactly when α is positive.

theorem LinearMap.IsSymmetric.norm_flow_neg_le_exp_mul_of_mem_negativeSpectralSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →L[ℝ] E} (hT : (↑T).IsSymmetric) (hn : Module.finrank ℝ E = n) {alpha t : ℝ} (halpha : ∀ (i : Fin n), hT.eigenvalues hn i < 0 → alpha ≤ -hT.eigenvalues hn i) (ht : t ≤ 0) {v : E} (hv : v ∈ hT.negativeSpectralSubspace hn) : ‖(-T).flow.toFun t v‖ ≤ Real.exp (alpha * t) * ‖v‖

For the flow generated by -T, a vector of the negative spectral subspace has norm at most exp (α t) * ‖v‖ in backward time, for any α below the absolute values of the negative eigenvalues. The bound decays exactly when α is positive.

theorem LinearMap.IsSymmetric.exists_exponential_bounds_spectralSubspaces {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →L[ℝ] E} (hT : (↑T).IsSymmetric) (hn : Module.finrank ℝ E = n) : ∃ alpha > 0, (∀ (t : ℝ), 0 ≤ t → ∀ v ∈ hT.positiveSpectralSubspace hn, ‖(-T).flow.toFun t v‖ ≤ Real.exp (-alpha * t) * ‖v‖) ∧ ∀ t ≤ 0, ∀ v ∈ hT.negativeSpectralSubspace hn, ‖(-T).flow.toFun t v‖ ≤ Real.exp (alpha * t) * ‖v‖

A symmetric operator has a common positive exponential contraction rate on its positive subspace in forward time and on its negative subspace in backward time. Zero eigenvalues are irrelevant because neither strict spectral subspace contains their eigendirections. The estimate has multiplicative constant one because the two subspaces are orthogonal sums of eigendirections.

theorem ContinuousLinearMap.IsIdempotentElem.exists_projection_exponential_bounds {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {alpha : ℝ} (hP : IsIdempotentElem P) (halpha : 0 < alpha) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ w ∈ (↑P).range, ‖(NormedSpace.exp (t • A)) w‖ ≤ Real.exp (-alpha * t) * ‖w‖) (hu : ∀ t ≤ 0, ∀ w ∈ (↑P).ker, ‖(NormedSpace.exp (t • A)) w‖ ≤ Real.exp (alpha * t) * ‖w‖) : ∃ (K : NNReal) (rate : NNReal), 0 < K ∧ 0 < rate ∧ (∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑rate * t) * ‖v‖) ∧ ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑rate * t) * ‖v‖

If an idempotent operator P has exponential flow bounds on its range and kernel, then it has the projection-form bounds used by the Lyapunov--Perron construction. The common constant absorbs the operator norms of P and 1 - P.