Linearization of the negative-gradient field at a Morse critical point #
The stable-manifold theorem starts with the derivative of the vector field at an equilibrium. For
a gradient field on a real Hilbert space, the second derivative of the function naturally takes
values in the continuous dual. The Riesz equivalence turns it into an endomorphism of the original
space, which is the derivative of the gradient: TauCeti.hessianOperator, the order-one field of
TauCeti.iteratedGradientChain.
At a twice continuously differentiable point this operator is self-adjoint, by symmetry of the
second derivative. At a nondegenerate critical point it is invertible, and the negative-gradient
field has derivative -hessianOperator f x. Consequently the field is its invertible linear part
up to a remainder of order o(‖y - x‖). The characterization
TauCeti.isNondegenerateCriticalPoint_iff_neg_gradient_linearization packages exactly the
equilibrium and invertible-linearization hypotheses needed for the stable-manifold theorem in the
gradient setting.
The definition uses Mathlib's totalized Fréchet derivative, just as
TauCeti.IsNondegenerateCriticalPoint and TauCeti.hessianQuadraticForm do. Regularity enters the
results that identify the operator as the derivative of the gradient and prove self-adjointness.
Main declarations #
TauCeti.hessianOperator: the Riesz-represented Hessian as an endomorphism of the Hilbert space.TauCeti.hessianOperator_eq_continuousLinearMapOfBilin: its Riesz formula.TauCeti.hessianOperator_congr_of_eventuallyEq: the operator depends only on the germ of the function at the point.ContDiffAt.isSelfAdjoint_hessianOperator: symmetry of the second derivative becomes self-adjointness of the Hessian operator.ContDiffAt.hasFDerivAt_neg_gradient: the derivative of-∇ fis the negative Hessian operator.TauCeti.negativeGradientRemainder: the nonlinear part of the negative-gradient field after subtracting its linearization at a chosen point.ContDiffAt.exists_lipschitzOnWith_negativeGradientRemainder: on a sufficiently small ball, the nonlinear remainder has any prescribed positive Lipschitz constant.ContDiffAt.neg_gradient_sub_linearization_isLittleO: at aC²critical point the nonlinear remainder after subtracting the linearization is little-o of the displacement.ContDiffAt.exists_norm_gradient_le_mul_norm_subandContDiffAt.exists_abs_sub_le_mul_norm_sub_sq: local upper estimates near a critical point.TauCeti.IsNondegenerateCriticalPoint.exists_mul_norm_sub_le_norm_gradientandTauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq: local lower and Łojasiewicz estimates near a nondegenerate critical point.TauCeti.isNondegenerateCriticalPoint_iff_neg_gradient_linearization: nondegenerate critical points are exactly the equilibria with invertible negative-gradient linearization, underC²regularity.
References #
- M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
The Hessian of f at x as an endomorphism of the Hilbert space: the order-one field
TauCeti.iteratedGradientChain f 1 of the iterated-gradient chain, that is, the Fréchet derivative
of the gradient. Its inner product with w is the second derivative of f evaluated on v, w.
The definition is meaningful without regularity because Mathlib's Fréchet derivative is totalized by zero. Twice continuous differentiability is assumed when this operator is used as the derivative of the gradient.
Equations
Instances For
The Fréchet derivative of the gradient is the Hessian operator, with no regularity assumption: both sides use Mathlib's totalized derivatives.
The Riesz formula for the Hessian operator: it is the endomorphism that the inner product
associates with the second derivative of f, viewed as a bilinear form.
The inner-product characterization of the Hessian operator.
Applying the Riesz map to the Hessian operator recovers the dual-valued second derivative.
The Hessian operator depends only on the germ of the function at the point.
Twice continuous differentiability makes the Hessian operator self-adjoint. This is the operator form of symmetry of the second Fréchet derivative.
The gradient is differentiable at a twice continuously differentiable point, with derivative the Hessian operator.
The negative-gradient vector field is differentiable at a twice continuously differentiable point, with derivative minus the Hessian operator.
The nonlinear remainder of the negative-gradient field after removing its linear part at x:
R_x(y) = -∇ f(y) + Hess_x(f)(y - x).
This convention does not subtract the constant value -∇ f x; at a critical point that value
vanishes, so R_x is exactly the first-order Taylor remainder. At a twice continuously
differentiable point its derivative at x is zero. The small local Lipschitz estimate for this
remainder is the nonlinear input to the Lyapunov--Perron construction of stable and unstable
manifolds.
Equations
- TauCeti.negativeGradientRemainder f x y = (-gradient f) y + (TauCeti.hessianOperator f x) (y - x)
Instances For
Evaluation of the negative-gradient remainder.
The negative-gradient field is its linearization plus its nonlinear remainder.
At a critical point, the nonlinear negative-gradient remainder vanishes at its base point.
The negative-gradient remainder is continuously differentiable at its base point when the function is twice continuously differentiable there.
At a twice continuously differentiable point, the derivative of the nonlinear negative-gradient remainder at its base point is zero.
At a twice continuously differentiable point, the nonlinear negative-gradient remainder is strictly differentiable with zero derivative. This is the two-point estimate needed by the contraction argument for the local stable-manifold theorem.
On a sufficiently small closed ball about a twice continuously differentiable point, the nonlinear negative-gradient remainder has any prescribed positive Lipschitz constant.
Unlike the one-point little-o estimate, this controls the difference of the remainder at two nearby points. It is therefore the estimate that makes the Lyapunov--Perron operator a contraction after its linear stable and unstable parts have been split.
At a critical point of a twice continuously differentiable function, the negative-gradient
field differs from its linearization by a term of order o(‖y - x‖). This is the nonlinear
remainder controlled in the local stable-manifold argument.
Near a critical point of a twice continuously differentiable function the gradient is bounded above by a multiple of the distance to that point: it vanishes at the point and is differentiable there.
Near a critical point of a twice continuously differentiable function the absolute energy
difference |f y - f x| is bounded by a multiple of the squared distance to that point. This is
the mean value inequality applied along the segment from x to y, on which the gradient is
bounded by a multiple of ‖y - x‖.
The Hessian operator is invertible exactly when the dual-valued second derivative is. Thus
the Hilbert-space operator formulation is equivalent to the Banach-space formulation used in
TauCeti.IsNondegenerateCriticalPoint.
The Hessian operator at a nondegenerate critical point is invertible.
The gradient vanishes at a nondegenerate critical point. This translates the dual-valued
criticality condition in TauCeti.IsNondegenerateCriticalPoint through the Riesz equivalence.
Negating a Hessian operator preserves and reflects invertibility.
The derivative of the negative-gradient field at a nondegenerate critical point is invertible.
The nonlinear-remainder estimate at a nondegenerate critical point.
Near a nondegenerate critical point the gradient is bounded below by a multiple of the distance to that point: the Hessian operator is invertible, hence bounded below, and the gradient differs from it by a term of smaller order.
The Morse form of Łojasiewicz's gradient inequality. Near a nondegenerate critical point
the absolute energy difference is bounded by a multiple of the squared norm of the gradient;
equivalently the Łojasiewicz inequality holds there with exponent 1 / 2.
Smoothness alone does not guarantee such an inequality, and a gradient trajectory can spiral
forever without converging.
On a real Hilbert space, nondegeneracy can be read entirely from the gradient and its Hessian operator.
A nondegenerate critical point is precisely an equilibrium of the negative-gradient field
whose derivative is invertible, under the stated C² regularity. This is the hyperbolicity input
to the stable-manifold theorem in the self-adjoint gradient setting.