Exponential bounds for a linearized Morse flow

The linearized negative-gradient flow contracts the positive Hessian subspace exponentially in forward time and the negative Hessian subspace exponentially in backward time, with one common positive rate. At a nondegenerate critical point these are the complementary stable and unstable linear subspaces, so the bounds form an exponential dichotomy.

This is the quantitative hyperbolicity estimate used by the Lyapunov--Perron proof of the local stable-manifold theorem. The subspaces and the qualitative identification of their asymptotic sets are provided by TauCeti.Analysis.Calculus.Morse.SpectralSplitting and TauCeti.Analysis.Calculus.Morse.HessianFlow; this file supplies the uniform spectral gap that turns convergence into contraction.

Main declaration

• ContDiffAt.exists_linearized_flow_exponential_bounds: the stable and unstable linearized flows contract exponentially with a common positive rate.
• ContDiffAt.exists_stableProjection_exponential_bounds: the same estimates in the projection form consumed by the Lyapunov--Perron construction.
• TauCeti.IsNondegenerateCriticalPoint.exists_stableProjection_exponential_bounds: the projection-form estimates specialized to the canonical projection at a nondegenerate critical point.

References

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

theorem ContDiffAt.exists_linearized_flow_exponential_bounds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : ∃ alpha > 0, (∀ (t : ℝ), 0 ≤ t → ∀ v ∈ hf.stableLinearSubspace, ‖(TauCeti.linearizedNegativeGradientFlow f x).toFun t v‖ ≤ Real.exp (-alpha * t) * ‖v‖) ∧ ∀ t ≤ 0, ∀ v ∈ hf.unstableLinearSubspace, ‖(TauCeti.linearizedNegativeGradientFlow f x).toFun t v‖ ≤ Real.exp (alpha * t) * ‖v‖

At a twice continuously differentiable point, the linearized negative-gradient flow contracts the positive Hessian subspace exponentially in forward time and the negative Hessian subspace exponentially in backward time. The same positive rate works in both directions.

theorem ContDiffAt.exists_stableProjection_exponential_bounds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hker : (↑(TauCeti.hessianOperator f x)).ker = ⊥) : ∃ (K : NNReal) (alpha : NNReal), 0 < K ∧ 0 < alpha ∧ (∀ (t : ℝ), 0 ≤ t → ∀ (v : E), ‖(NormedSpace.exp (t • -TauCeti.hessianOperator f x)) ((hf.stableProjection hker) v)‖ ≤ ↑K * Real.exp (-↑alpha * t) * ‖v‖) ∧ ∀ t ≤ 0, ∀ (v : E), ‖(NormedSpace.exp (t • -TauCeti.hessianOperator f x)) (v - (hf.stableProjection hker) v)‖ ≤ ↑K * Real.exp (↑alpha * t) * ‖v‖

When the Hessian is injective, the stable projection gives an exponential dichotomy for the negative Hessian operator. The common constant K absorbs the operator norms of the projection and its complementary projection.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_stableProjection_exponential_bounds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : ∃ (K : NNReal) (alpha : NNReal), 0 < K ∧ 0 < alpha ∧ (∀ (t : ℝ), 0 ≤ t → ∀ (v : E), ‖(NormedSpace.exp (t • -hessianOperator f x)) (h.stableProjection v)‖ ≤ ↑K * Real.exp (-↑alpha * t) * ‖v‖) ∧ ∀ t ≤ 0, ∀ (v : E), ‖(NormedSpace.exp (t • -hessianOperator f x)) (v - h.stableProjection v)‖ ≤ ↑K * Real.exp (↑alpha * t) * ‖v‖

At a nondegenerate critical point, the canonical stable projection gives an exponential dichotomy for the negative Hessian operator.