Spectral splitting at a Morse critical point

At a nondegenerate critical point on a finite-dimensional real Hilbert space, the Hessian is an invertible self-adjoint operator. Its positive and negative spectral subspaces therefore give a direct-sum decomposition of the tangent space. For the negative-gradient vector field, the positive Hessian subspace is the stable linear subspace and the negative Hessian subspace is the unstable linear subspace.

This file constructs those two subspaces, shows that both are invariant under the negative-gradient linearization, and identifies the dimension of the unstable subspace with the Morse index; the stable dimension and the Morse index therefore add up to the dimension of the ambient space.

These are the linear data used by the local stable- and unstable-manifold theorems. No local invariant manifold is asserted here: those theorems additionally have to control the nonlinear remainder of the negative-gradient field, supplied by TauCeti.IsNondegenerateCriticalPoint.neg_gradient_sub_linearization_isLittleO.

Main declarations

• ContDiffAt.stableLinearSubspace: the positive spectral subspace of the Hessian.
• ContDiffAt.unstableLinearSubspace: the negative spectral subspace of the Hessian.
• ContDiffAt.map_neg_hessianOperator_stableLinearSubspace_le and ContDiffAt.map_neg_hessianOperator_unstableLinearSubspace_le: both subspaces are invariant under the negative-gradient linearization -hessianOperator f x.
• ContDiffAt.isCompl_unstableLinearSubspace_stableLinearSubspace: when the Hessian is injective these subspaces are complementary, so the tangent space is their direct sum.
• ContDiffAt.finrank_unstableLinearSubspace: the unstable dimension is the Morse index.
• ContDiffAt.finrank_stableLinearSubspace_add_morseIndex: the stable dimension plus the Morse index is the ambient dimension.
• TauCeti.IsNondegenerateCriticalPoint.isCompl_unstableLinearSubspace_stableLinearSubspace and TauCeti.IsNondegenerateCriticalPoint.finrank_stableLinearSubspace_add_morseIndex: the same two results stated for a nondegenerate critical point, which supplies the Hessian injectivity.
• ContDiffAt.stableProjection: when the Hessian is injective, the continuous projection onto the stable linear subspace along the unstable linear subspace.
• ContDiffAt.unstableProjection: the complementary projection onto the unstable linear subspace along the stable linear subspace.
• TauCeti.IsNondegenerateCriticalPoint.stableProjection and TauCeti.IsNondegenerateCriticalPoint.unstableProjection: the same two projections specialized to a nondegenerate critical point, which supplies Hessian injectivity.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
• J. Milnor, Morse Theory, Princeton University Press, 1963, §2.

noncomputable def ContDiffAt.stableLinearSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Submodule ℝ E

The stable linear subspace of the negative-gradient field at a C² point: the span of the Hessian eigenvectors with positive eigenvalues. The linear flow generated by -hessianOperator f x contracts these directions.

Equations

• hf.stableLinearSubspace = ⋯.positiveSpectralSubspace ⋯

noncomputable def ContDiffAt.unstableLinearSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Submodule ℝ E

The unstable linear subspace of the negative-gradient field at a C² point: the span of the Hessian eigenvectors with negative eigenvalues. The linear flow generated by -hessianOperator f x expands these directions in forward time.

Equations

• hf.unstableLinearSubspace = ⋯.negativeSpectralSubspace ⋯

@[simp]

theorem ContDiffAt.mem_stableLinearSubspace_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) {v : E} : v ∈ hf.stableLinearSubspace ↔ ∀ i ∈ ((⋯.eigenvectorBasis ⋯).toBasis.repr v).support, 0 < ⋯.eigenvalues ⋯ i

A vector is stable exactly when its Hessian eigenbasis representation is supported on the positive eigenvalues.

@[simp]

theorem ContDiffAt.mem_unstableLinearSubspace_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) {v : E} : v ∈ hf.unstableLinearSubspace ↔ ∀ i ∈ ((⋯.eigenvectorBasis ⋯).toBasis.repr v).support, ⋯.eigenvalues ⋯ i < 0

A vector is unstable exactly when its Hessian eigenbasis representation is supported on the negative eigenvalues.

theorem ContDiffAt.map_hessianOperator_stableLinearSubspace_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Submodule.map (↑(TauCeti.hessianOperator f x)) hf.stableLinearSubspace ≤ hf.stableLinearSubspace

The Hessian preserves the stable linear subspace.

theorem ContDiffAt.map_hessianOperator_unstableLinearSubspace_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Submodule.map (↑(TauCeti.hessianOperator f x)) hf.unstableLinearSubspace ≤ hf.unstableLinearSubspace

The Hessian preserves the unstable linear subspace.

theorem ContDiffAt.map_neg_hessianOperator_stableLinearSubspace_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Submodule.map (↑(-TauCeti.hessianOperator f x)) hf.stableLinearSubspace ≤ hf.stableLinearSubspace

The negative-gradient linearization preserves the stable linear subspace. It is -hessianOperator f x, the derivative of -∇ f at x by ContDiffAt.hasFDerivAt_neg_gradient.

theorem ContDiffAt.map_neg_hessianOperator_unstableLinearSubspace_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Submodule.map (↑(-TauCeti.hessianOperator f x)) hf.unstableLinearSubspace ≤ hf.unstableLinearSubspace

The negative-gradient linearization preserves the unstable linear subspace. It is -hessianOperator f x, the derivative of -∇ f at x by ContDiffAt.hasFDerivAt_neg_gradient.

theorem ContDiffAt.disjoint_unstableLinearSubspace_stableLinearSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Disjoint hf.unstableLinearSubspace hf.stableLinearSubspace

The stable and unstable linear subspaces at a C² point are disjoint. This does not require nondegeneracy: the zero eigenspace belongs to neither subspace.

theorem ContDiffAt.morseIndex_eq_ncard_hessianOperator_eigenvalues_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : TauCeti.morseIndex f x = {i : Fin (Module.finrank ℝ E) | ⋯.eigenvalues ⋯ i < 0}.ncard

In the Hessian eigenbasis, the number of negative eigenvalues, counted with multiplicity, is the Morse index.

@[simp]

theorem ContDiffAt.finrank_unstableLinearSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) : Module.finrank ℝ ↥hf.unstableLinearSubspace = TauCeti.morseIndex f x

The dimension of the unstable linear subspace at a C² point is its Morse index.

theorem ContDiffAt.isCompl_unstableLinearSubspace_stableLinearSubspace {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 = ⊥) : IsCompl hf.unstableLinearSubspace hf.stableLinearSubspace

When the Hessian is injective, the unstable and stable linear subspaces are complementary, so the tangent space is their direct sum. Injectivity excludes the zero eigenspace; at a nondegenerate critical point it comes from TauCeti.IsNondegenerateCriticalPoint.isInvertible_hessianOperator.

theorem ContDiffAt.finrank_stableLinearSubspace_add_morseIndex {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 = ⊥) : Module.finrank ℝ ↥hf.stableLinearSubspace + TauCeti.morseIndex f x = Module.finrank ℝ E

When the Hessian is injective, the dimension of the stable linear subspace plus the Morse index is the dimension of the ambient tangent space.

noncomputable def ContDiffAt.stableProjection {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 = ⊥) : E →L[ℝ] E

When the Hessian is injective, the continuous projection onto the stable linear subspace along the unstable linear subspace.

Equations

• hf.stableProjection hker = hf.stableLinearSubspace.projectionL hf.unstableLinearSubspace ⋯

@[simp]

theorem ContDiffAt.range_stableProjection {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 = ⊥) : (↑(hf.stableProjection hker)).range = hf.stableLinearSubspace

The range of the stable projection is the stable linear subspace.

@[simp]

theorem ContDiffAt.ker_stableProjection {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 = ⊥) : (↑(hf.stableProjection hker)).ker = hf.unstableLinearSubspace

The kernel of the stable projection is the unstable linear subspace.

theorem ContDiffAt.isIdempotentElem_stableProjection {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 = ⊥) : IsIdempotentElem (hf.stableProjection hker)

The stable projection is idempotent.

@[simp]

theorem ContDiffAt.stableProjection_apply_eq_zero_iff {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 = ⊥) {v : E} : (hf.stableProjection hker) v = 0 ↔ v ∈ hf.unstableLinearSubspace

A vector is killed by the stable projection exactly when it is unstable.

@[simp]

theorem ContDiffAt.stableProjection_apply_eq_self_iff {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 = ⊥) {v : E} : (hf.stableProjection hker) v = v ↔ v ∈ hf.stableLinearSubspace

A vector is fixed by the stable projection exactly when it is stable.

theorem ContDiffAt.stableProjection_apply_mem {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 = ⊥) (v : E) : (hf.stableProjection hker) v ∈ hf.stableLinearSubspace

The stable projection takes every vector into the stable linear subspace.

theorem ContDiffAt.commute_neg_hessianOperator_stableProjection {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 = ⊥) : Commute (-TauCeti.hessianOperator f x) (hf.stableProjection hker)

The negative Hessian operator commutes with the projection onto its stable linear subspace.

noncomputable def ContDiffAt.unstableProjection {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 = ⊥) : E →L[ℝ] E

When the Hessian is injective, the continuous projection onto the unstable linear subspace along the stable linear subspace: the projection complementary to ContDiffAt.stableProjection.

Equations

• hf.unstableProjection hker = ContinuousLinearMap.id ℝ E - hf.stableProjection hker

theorem ContDiffAt.unstableProjection_def {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 = ⊥) : hf.unstableProjection hker = ContinuousLinearMap.id ℝ E - hf.stableProjection hker

The unstable projection is the identity minus the stable projection.

theorem ContDiffAt.unstableProjection_apply {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 = ⊥) (v : E) : (hf.unstableProjection hker) v = v - (hf.stableProjection hker) v

The unstable projection subtracts the stable component.

theorem ContDiffAt.isIdempotentElem_unstableProjection {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 = ⊥) : IsIdempotentElem (hf.unstableProjection hker)

The unstable projection is idempotent.

@[simp]

theorem ContDiffAt.range_unstableProjection {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 = ⊥) : (↑(hf.unstableProjection hker)).range = hf.unstableLinearSubspace

The range of the unstable projection is the unstable linear subspace.

@[simp]

theorem ContDiffAt.ker_unstableProjection {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 = ⊥) : (↑(hf.unstableProjection hker)).ker = hf.stableLinearSubspace

The kernel of the unstable projection is the stable linear subspace.

@[simp]

theorem ContDiffAt.unstableProjection_apply_eq_zero_iff {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 = ⊥) {v : E} : (hf.unstableProjection hker) v = 0 ↔ v ∈ hf.stableLinearSubspace

A vector is killed by the unstable projection exactly when it is stable.

@[simp]

theorem ContDiffAt.unstableProjection_apply_eq_self_iff {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 = ⊥) {v : E} : (hf.unstableProjection hker) v = v ↔ v ∈ hf.unstableLinearSubspace

A vector is fixed by the unstable projection exactly when it is unstable.

theorem ContDiffAt.unstableProjection_apply_mem {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 = ⊥) (v : E) : (hf.unstableProjection hker) v ∈ hf.unstableLinearSubspace

The unstable projection takes every vector into the unstable linear subspace.

theorem ContDiffAt.commute_neg_hessianOperator_unstableProjection {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 = ⊥) : Commute (-TauCeti.hessianOperator f x) (hf.unstableProjection hker)

The negative Hessian operator commutes with the projection onto its unstable linear subspace.

theorem TauCeti.IsNondegenerateCriticalPoint.isCompl_unstableLinearSubspace_stableLinearSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : IsCompl ⋯.unstableLinearSubspace ⋯.stableLinearSubspace

At a nondegenerate critical point the unstable and stable linear subspaces are complementary, so the tangent space is their direct sum.

theorem TauCeti.IsNondegenerateCriticalPoint.finrank_stableLinearSubspace_add_morseIndex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : Module.finrank ℝ ↥⋯.stableLinearSubspace + morseIndex f x = Module.finrank ℝ E

At a nondegenerate critical point the dimension of the stable linear subspace plus the Morse index is the dimension of the ambient tangent space.

noncomputable def TauCeti.IsNondegenerateCriticalPoint.stableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : E →L[ℝ] E

The continuous projection onto the stable linear subspace at a nondegenerate critical point, along the unstable linear subspace.

Equations

• h.stableProjection = ⋯.stableProjection ⋯

noncomputable def TauCeti.IsNondegenerateCriticalPoint.unstableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : E →L[ℝ] E

The continuous projection onto the unstable linear subspace at a nondegenerate critical point, complementary to stableProjection.

Equations

• h.unstableProjection = ContinuousLinearMap.id ℝ E - h.stableProjection

theorem TauCeti.IsNondegenerateCriticalPoint.unstableProjection_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : h.unstableProjection = ContinuousLinearMap.id ℝ E - h.stableProjection

The unstable projection is the complementary projection to the stable projection.

theorem TauCeti.IsNondegenerateCriticalPoint.unstableProjection_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (v : E) : h.unstableProjection v = v - h.stableProjection v

The unstable projection is the identity minus the stable projection.

theorem TauCeti.IsNondegenerateCriticalPoint.stableProjection_eq_contDiffAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : h.stableProjection = ⋯.stableProjection ⋯

The stable projection at a nondegenerate critical point is the general stable projection formed using the Hessian injectivity supplied by nondegeneracy.

theorem TauCeti.IsNondegenerateCriticalPoint.unstableProjection_eq_contDiffAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : h.unstableProjection = ⋯.unstableProjection ⋯

The unstable projection at a nondegenerate critical point is the general unstable projection formed using the Hessian injectivity supplied by nondegeneracy.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.range_stableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : (↑h.stableProjection).range = ⋯.stableLinearSubspace

The range of the stable projection at a nondegenerate critical point is the stable linear subspace.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.ker_stableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : (↑h.stableProjection).ker = ⋯.unstableLinearSubspace

The kernel of the stable projection at a nondegenerate critical point is the unstable linear subspace.

theorem TauCeti.IsNondegenerateCriticalPoint.isIdempotentElem_stableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : IsIdempotentElem h.stableProjection

The stable projection at a nondegenerate critical point is idempotent.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.range_unstableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : (↑h.unstableProjection).range = ⋯.unstableLinearSubspace

The range of the unstable projection is the unstable linear subspace.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.ker_unstableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : (↑h.unstableProjection).ker = ⋯.stableLinearSubspace

The kernel of the unstable projection is the stable linear subspace.

theorem TauCeti.IsNondegenerateCriticalPoint.isIdempotentElem_unstableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : IsIdempotentElem h.unstableProjection

The unstable projection is idempotent.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.stableProjection_apply_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) {v : E} : h.stableProjection v = 0 ↔ v ∈ ⋯.unstableLinearSubspace

A vector is killed by the stable projection at a nondegenerate critical point exactly when it is unstable.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.stableProjection_apply_eq_self_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) {v : E} : h.stableProjection v = v ↔ v ∈ ⋯.stableLinearSubspace

A vector is fixed by the stable projection at a nondegenerate critical point exactly when it is stable.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.unstableProjection_apply_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) {v : E} : h.unstableProjection v = 0 ↔ v ∈ ⋯.stableLinearSubspace

A vector is killed by the unstable projection exactly when it is stable.

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.unstableProjection_apply_eq_self_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) {v : E} : h.unstableProjection v = v ↔ v ∈ ⋯.unstableLinearSubspace

A vector is fixed by the unstable projection exactly when it is unstable.

theorem TauCeti.IsNondegenerateCriticalPoint.unstableProjection_apply_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (v : E) : h.unstableProjection v ∈ ⋯.unstableLinearSubspace

The unstable projection takes every vector into the unstable linear subspace.

theorem TauCeti.IsNondegenerateCriticalPoint.stableProjection_apply_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) (v : E) : h.stableProjection v ∈ ⋯.stableLinearSubspace

The stable projection at a nondegenerate critical point takes every vector into the stable linear subspace.

theorem TauCeti.IsNondegenerateCriticalPoint.commute_neg_hessianOperator_stableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : Commute (-hessianOperator f x) h.stableProjection

The negative Hessian operator commutes with the stable projection at a nondegenerate critical point.

theorem TauCeti.IsNondegenerateCriticalPoint.commute_neg_hessianOperator_unstableProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (h : IsNondegenerateCriticalPoint f x) : Commute (-hessianOperator f x) h.unstableProjection

The negative Hessian operator commutes with the unstable projection at a nondegenerate critical point.