The linearized negative-gradient flow at a Morse critical point

The derivative of the negative-gradient field at a twice continuously differentiable point is the negative Hessian operator. Exponentiating this operator gives the linear flow that models the gradient flow near a critical point.

This file identifies the stable and unstable sets of that flow exactly. The stable set is the positive Hessian spectral subspace, while the unstable set is the negative Hessian spectral subspace. At a nondegenerate critical point these are the complementary subspaces constructed in TauCeti.Analysis.Calculus.Morse.SpectralSplitting; the nonlinear stable-manifold theorem should produce local invariant manifolds tangent to them.

Main declarations

• TauCeti.linearizedNegativeGradientFlow: the exponential flow generated by the negative Hessian operator.
• ContDiffAt.stableSet_linearizedNegativeGradientFlow: its stable set is the stable linear subspace.
• ContDiffAt.unstableSet_linearizedNegativeGradientFlow: its unstable set is the unstable linear subspace.

References

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

noncomputable def TauCeti.linearizedNegativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) : Flow ℝ E

The linearized negative-gradient flow of f at x. Its time-t map is exp (-t • hessianOperator f x). Regularity is not required for the definition because the Fréchet derivative, and hence hessianOperator, is totalized by zero.

Equations

• TauCeti.linearizedNegativeGradientFlow f x = (-TauCeti.hessianOperator f x).flow

@[simp]

theorem TauCeti.linearizedNegativeGradientFlow_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : E → ℝ) (x : E) (t : ℝ) (v : E) : (linearizedNegativeGradientFlow f x).toFun t v = (NormedSpace.exp (-t • hessianOperator f x)) v

The time-t map of the linearized negative-gradient flow is the exponential of -t times the Hessian operator.

@[simp]

theorem ContDiffAt.stableSet_linearizedNegativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : (TauCeti.linearizedNegativeGradientFlow f x).stableSet 0 = ↑hf.stableLinearSubspace

The stable set of zero for the linearized negative-gradient flow is exactly the positive Hessian spectral subspace.

@[simp]

theorem ContDiffAt.unstableSet_linearizedNegativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : (TauCeti.linearizedNegativeGradientFlow f x).unstableSet 0 = ↑hf.unstableLinearSubspace

The unstable set of zero for the linearized negative-gradient flow is exactly the negative Hessian spectral subspace.