Embedded local Lyapunov--Perron graphs

The local stable and unstable sets of a hyperbolic equilibrium are described in LyapunovPerron.Local as graphs over complementary spectral subspaces. This file records that these descriptions are actual topological embeddings: projection onto the relevant spectral subspace is the continuous inverse of the graph parameterization on its image.

This supplies the topological parameterizations used when passing from local invariant sets to the stable and unstable manifolds used in Morse trajectory spaces.

Main declarations

• ContinuousLinearMap.localStableSetHomeomorph and ContinuousLinearMap.localUnstableSetHomeomorph parameterize the confined local invariant sets by closed balls in their respective spectral subspaces.
• ContinuousLinearMap.exists_localStableSetHomeomorph and ContinuousLinearMap.exists_localUnstableSetHomeomorph supply a truncation radius for which those parameterizations exist, so that a caller with a ball of confinement need not produce one.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
• C. Chicone, Ordinary Differential Equations with Applications, 2nd ed., Springer, 2006, Section 4.3.

noncomputable def ContinuousLinearMap.localStableSetHomeomorph {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hr : 0 ≤ r) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) {ρ : ℝ} (hρ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r) : ↑{v : ↑(Set.range ⇑P) | ‖↑v‖ ≤ ρ} ≃ₜ ↑{x : X | (∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Ici 0) ∧ y 0 = x ∧ Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) ∧ ‖P x‖ ≤ ρ}

The local stable set of confined forward solutions, truncated by the norm of its stable projection, is homeomorphic to the corresponding closed ball in the stable spectral subspace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.coe_localStableSetHomeomorph_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hr : 0 ≤ r) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) {ρ : ℝ} (hρ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r) (v : ↑{v : ↑(Set.range ⇑P) | ‖↑v‖ ≤ ρ}) : ↑((A.localStableSetHomeomorph P N r hs hu hr hN hsmall hN0 hP hAP hρ) v) = ↑↑v + A.localStableGraphMap P N r hs hu hr hN hsmall ↑↑v

The local stable set homeomorphism is the graph parameterization v ↦ v + h(v).

@[simp]

theorem ContinuousLinearMap.coe_localStableSetHomeomorph_symm_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hr : 0 ≤ r) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) {ρ : ℝ} (hρ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r) (x : ↑{x : X | (∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Ici 0) ∧ y 0 = x ∧ Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) ∧ ‖P x‖ ≤ ρ}) : ↑↑((A.localStableSetHomeomorph P N r hs hu hr hN hsmall hN0 hP hAP hρ).symm x) = P ↑x

The inverse of the local stable set homeomorphism is the stable projection.

noncomputable def ContinuousLinearMap.localUnstableSetHomeomorph {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hr : 0 ≤ r) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) {ρ : ℝ} (hρ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r) : ↑{v : ↑(Set.range ⇑(ContinuousLinearMap.id ℝ X - P)) | ‖↑v‖ ≤ ρ} ≃ₜ ↑{x : X | (∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Iic 0) ∧ y 0 = x ∧ Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r)) ∧ ‖(ContinuousLinearMap.id ℝ X - P) x‖ ≤ ρ}

The local unstable set of confined backward solutions, truncated by the norm of its complementary projection, is homeomorphic to the corresponding closed ball in the unstable spectral subspace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.coe_localUnstableSetHomeomorph_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hr : 0 ≤ r) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) {ρ : ℝ} (hρ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r) (v : ↑{v : ↑(Set.range ⇑(ContinuousLinearMap.id ℝ X - P)) | ‖↑v‖ ≤ ρ}) : ↑((A.localUnstableSetHomeomorph P N r hs hu hr hN hsmall hN0 hP hAP hρ) v) = ↑↑v + A.localUnstableGraphMap P N r hs hu hr hN hsmall ↑↑v

The local unstable set homeomorphism is the graph parameterization v ↦ v + h(v).

@[simp]

theorem ContinuousLinearMap.coe_localUnstableSetHomeomorph_symm_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hr : 0 ≤ r) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) {ρ : ℝ} (hρ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r) (x : ↑{x : X | (∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Iic 0) ∧ y 0 = x ∧ Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r)) ∧ ‖(ContinuousLinearMap.id ℝ X - P) x‖ ≤ ρ}) : ↑↑((A.localUnstableSetHomeomorph P N r hs hu hr hN hsmall hN0 hP hAP hρ).symm x) = (ContinuousLinearMap.id ℝ X - P) ↑x

The inverse of the local unstable set homeomorphism is the unstable projection.

theorem ContinuousLinearMap.exists_localStableSetHomeomorph {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) (hr0 : 0 < r) : ∃ ρ > 0, Nonempty (↑{v : ↑(Set.range ⇑P) | ‖↑v‖ ≤ ρ} ≃ₜ ↑{z : X | (∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (w : X) => A w + N w) (Set.Ici 0) ∧ y 0 = z ∧ Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) ∧ ‖P z‖ ≤ ρ})

For a small enough truncation radius, the local stable set of confined forward solutions is homeomorphic to a closed ball in the stable spectral subspace.

theorem ContinuousLinearMap.exists_localUnstableSetHomeomorph {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} (A P : X →L[ℝ] X) (N : X → X) (r : ℝ) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0) (hP : IsIdempotentElem P) (hAP : Commute A P) (hr0 : 0 < r) : ∃ ρ > 0, Nonempty (↑{v : ↑(Set.range ⇑(ContinuousLinearMap.id ℝ X - P)) | ‖↑v‖ ≤ ρ} ≃ₜ ↑{z : X | (∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (w : X) => A w + N w) (Set.Iic 0) ∧ y 0 = z ∧ Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r)) ∧ ‖(ContinuousLinearMap.id ℝ X - P) z‖ ≤ ρ})

For a small enough truncation radius, the local unstable set of confined backward solutions is homeomorphic to a closed ball in the unstable spectral subspace.