The split quadratic model of a Morse flow

This file studies the standard split-quadratic example of a negative-gradient flow. On a product of real Hilbert spaces, put

q(x, y) = (‖x‖² - ‖y‖²) / 2.

Its gradient is (x, -y), so its negative-gradient flow is

φ t (x, y) = (exp (-t) • x, exp t • y).

This file constructs that flow and computes its stable and unstable sets exactly. The stable set of the origin is the first coordinate plane and the unstable set is the second coordinate plane. Thus the two sets in this normalized linear example are genuine closed linear subspaces, rather than only sets defined by asymptotic convergence. For a general Morse critical point, the metric and Hessian determine the corresponding linearized gradient flow and its contraction rates.

Main declarations

• TauCeti.splitQuadratic: the standard split quadratic function.
• TauCeti.gradient_splitQuadratic: its gradient is (x, -y).
• TauCeti.lipschitzWith_gradient_splitQuadratic: its gradient is globally 1-Lipschitz.
• TauCeti.isNondegenerateCriticalPoint_splitQuadratic_zero: the origin is nondegenerate.
• TauCeti.splitQuadraticFlow: its explicit negative-gradient flow.
• Flow.isNegativeGradient_splitQuadraticFlow: the flow solves the negative-gradient equation.
• TauCeti.negativeGradientFlow_splitQuadratic: the general construction of the negative gradient flow returns this explicit flow.
• Flow.stableSet_splitQuadraticFlow_zero: the stable set is the first coordinate plane.
• Flow.unstableSet_splitQuadraticFlow_zero: the unstable set is the second coordinate plane.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapters 1--2.
• Heegaard Floer homology roadmap, Lane M, "Morse homology".

noncomputable def TauCeti.splitQuadratic {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : ℝ

The standard split quadratic function, positive on the first factor and negative on the second. The factor 2⁻¹ normalizes its gradient to (x, -y).

Equations

• TauCeti.splitQuadratic z = (‖z.fst‖ ^ 2 - ‖z.snd‖ ^ 2) / 2

@[simp]

theorem TauCeti.splitQuadratic_apply {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : splitQuadratic z = (‖z.fst‖ ^ 2 - ‖z.snd‖ ^ 2) / 2

Evaluation of the standard split quadratic function.

theorem TauCeti.hasGradientAt_splitQuadratic {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : HasGradientAt splitQuadratic (WithLp.toLp 2 (z.fst, -z.snd)) z

The gradient of the split quadratic function is the identity on the first factor and minus the identity on the second.

@[simp]

theorem TauCeti.gradient_splitQuadratic {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : gradient splitQuadratic z = WithLp.toLp 2 (z.fst, -z.snd)

Formula for the gradient of the split quadratic function.

theorem TauCeti.gradient_splitQuadratic_eq_zero_iff {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : gradient splitQuadratic z = 0 ↔ z = 0

The origin is the unique critical point of the split quadratic function.

theorem TauCeti.lipschitzWith_gradient_splitQuadratic {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] : LipschitzWith 1 (gradient splitQuadratic)

The gradient of the split quadratic function is an isometry of the underlying space, hence in particular globally 1-Lipschitz. This is the hypothesis under which the negative gradient flow of a function exists on the whole line.

theorem TauCeti.isNondegenerateCriticalPoint_splitQuadratic_zero {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] : IsNondegenerateCriticalPoint splitQuadratic 0

The origin is a nondegenerate critical point of the split quadratic function.

noncomputable def TauCeti.splitQuadraticFlow {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [NormedSpace ℝ Eₛ] [NormedSpace ℝ Eᵤ] : Flow ℝ (WithLp 2 (Eₛ × Eᵤ))

The explicit hyperbolic flow of the split quadratic function. Its first coordinate contracts in forward time and its second coordinate contracts in backward time.

Equations

• TauCeti.splitQuadraticFlow = { toFun := fun (t : ℝ) (z : WithLp 2 (Eₛ × Eᵤ)) => WithLp.toLp 2 (Real.exp (-t) • z.fst, Real.exp t • z.snd), cont' := ⋯, map_add' := ⋯, map_zero' := ⋯ }

@[simp]

theorem TauCeti.splitQuadraticFlow_apply {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [NormedSpace ℝ Eₛ] [NormedSpace ℝ Eᵤ] (t : ℝ) (z : WithLp 2 (Eₛ × Eᵤ)) : splitQuadraticFlow.toFun t z = WithLp.toLp 2 (Real.exp (-t) • z.fst, Real.exp t • z.snd)

Evaluation of the split quadratic flow.

theorem Flow.isNegativeGradient_splitQuadraticFlow {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] : TauCeti.splitQuadraticFlow.IsNegativeGradient TauCeti.splitQuadratic

Every orbit of the explicit split flow solves the negative-gradient equation for TauCeti.splitQuadratic.

theorem TauCeti.negativeGradientFlow_splitQuadratic {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [InnerProductSpace ℝ Eₛ] [InnerProductSpace ℝ Eᵤ] [CompleteSpace Eₛ] [CompleteSpace Eᵤ] : negativeGradientFlow splitQuadratic ⋯ = splitQuadraticFlow

On the split quadratic model, the negative gradient flow built from a globally Lipschitz gradient is the explicit hyperbolic flow.

theorem TauCeti.tendsto_splitQuadraticFlow_atTop_nhds_zero_iff {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [NormedSpace ℝ Eₛ] [NormedSpace ℝ Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : Filter.Tendsto (fun (t : ℝ) => splitQuadraticFlow.toFun t z) Filter.atTop (nhds 0) ↔ z.snd = 0

A point converges to the origin in forward time exactly when its expanding coordinate vanishes.

theorem TauCeti.tendsto_splitQuadraticFlow_atBot_nhds_zero_iff {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [NormedSpace ℝ Eₛ] [NormedSpace ℝ Eᵤ] (z : WithLp 2 (Eₛ × Eᵤ)) : Filter.Tendsto (fun (t : ℝ) => splitQuadraticFlow.toFun t z) Filter.atBot (nhds 0) ↔ z.fst = 0

A point converges to the origin in backward time exactly when its expanding-backward coordinate vanishes.

@[simp]

theorem Flow.stableSet_splitQuadraticFlow_zero {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [NormedSpace ℝ Eₛ] [NormedSpace ℝ Eᵤ] : TauCeti.splitQuadraticFlow.stableSet 0 = {z : WithLp 2 (Eₛ × Eᵤ) | z.snd = 0}

The stable set of the split quadratic flow at the origin is the first coordinate plane.

@[simp]

theorem Flow.unstableSet_splitQuadraticFlow_zero {Eₛ : Type u_1} {Eᵤ : Type u_2} [NormedAddCommGroup Eₛ] [NormedAddCommGroup Eᵤ] [NormedSpace ℝ Eₛ] [NormedSpace ℝ Eᵤ] : TauCeti.splitQuadraticFlow.unstableSet 0 = {z : WithLp 2 (Eₛ × Eᵤ) | z.fst = 0}

The unstable set of the split quadratic flow at the origin is the second coordinate plane.