Local stable and unstable sets at a hyperbolic equilibrium

TauCeti/Analysis/ODE/LyapunovPerron/Graph.lean describes the stable set of the equilibrium 0 of y' = A y + N y for a nonlinearity N that is globally Lipschitz with a constant small compared to the spectral gap of A. A nonlinearity coming from a vector field with a hyperbolic equilibrium is not of that form: it is only small near the equilibrium, where the field is close to its linearization. This file bridges the two by cutting the nonlinearity off outside a closed ball of radius r, using the radial retraction of TauCeti/Analysis/Normed/Module/Ball/Retraction.lean.

Cutting off replaces N by N ∘ radialRetraction r, which agrees with N on the ball, preserves the value of N at the origin, and is globally Lipschitz with twice the constant that N has on the ball. Feeding it to the Lyapunov--Perron machinery produces ContinuousLinearMap.localStableGraphMap, a Lipschitz map into the kernel of P. Under the stated bound on ρ, the local stable set truncated by ‖P x‖ ≤ ρ is its graph over range P ∩ closedBall 0 ρ: these are the initial values of the forward solutions of y' = A y + N y that never leave the ball of radius r. Confinement already forces such a solution to tend to 0, so the set deserves its name.

The two descriptions match exactly where the cutoff is invisible. A confined forward solution of the original equation solves the cut-off equation as well, so it always lies on the graph; and conversely a point of the graph whose P-component v is small enough that the uniform bound ‖y t‖ ≤ K / (1 - 2 K (2 ε) / α) ‖v‖ on Lyapunov--Perron solutions keeps y inside the ball carries a confined solution. If N has derivative zero at the equilibrium, the graph map does too: although the radial cutoff need not be differentiable at the boundary sphere, it agrees with N near zero, and the Lyapunov--Perron solutions tend uniformly to zero with their input parameter. Together with ContinuousLinearMap.apply_localStableGraphMap, this makes the graph tangent to the range of P at the equilibrium whenever P is the commuting projection of an exponential dichotomy. If N is C¹ on the open ball, with derivative uniformly continuous there, the graph map is C¹ at every parameter v small enough that the same uniform bound keeps the solution strictly inside the ball: there the cut-off nonlinearity is N near every value of the solution, and ContinuousLinearMap.contDiffAt_lyapunovPerronGraphMap applies.

Time reversal applies the same construction to -A, -N, and the complementary projection 1 - P, without duplicating the fixed-point argument. When P is idempotent this gives the local unstable set as a Lipschitz graph over range (1 - P), and when P moreover commutes with A the graph map takes its values in range P. Its derivative also vanishes at the equilibrium when the derivative of N does, and it is C¹ near the equilibrium when N is.

Main declarations

• ContinuousLinearMap.localStableGraphMap: the Lyapunov--Perron graph map of the cut-off nonlinearity, with ContinuousLinearMap.lipschitzWith_localStableGraphMap and ContinuousLinearMap.norm_localStableGraphMap_le for its Lipschitz constant and cone bound.
• ContinuousLinearMap.hasFDerivAt_localStableGraphMap_zero and ContinuousLinearMap.hasFDerivAt_localUnstableGraphMap_zero: when the nonlinear remainder has derivative zero at the equilibrium, so do the local stable and unstable graph maps.
• ContinuousLinearMap.contDiffAt_localStableGraphMap and ContinuousLinearMap.contDiffAt_localUnstableGraphMap: when the nonlinear remainder is C¹ on the ball of confinement, with uniformly continuous derivative, the local stable and unstable graph maps are C¹ at every parameter whose solution stays strictly inside that ball.
• ContinuousLinearMap.tendsto_of_isIntegralCurveOn_mapsTo_closedBall: a forward solution that never leaves the ball of radius r tends to the equilibrium.
• ContinuousLinearMap.setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image: the local stable set, cut down to where the P-component has norm at most ρ, is the graph of that map over the closed ball of radius ρ in the range of P, for every ρ small enough.
• ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image: such a ρ exists as soon as the ball of confinement has positive radius, by the radius choice of TauCeti.exists_pos_lyapunovPerronBound_mul_le.
• ContinuousLinearMap.localUnstableGraphMap, with ContinuousLinearMap.lipschitzWith_localUnstableGraphMap and ContinuousLinearMap.norm_localUnstableGraphMap_le, ContinuousLinearMap.setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image and ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image: the corresponding graph and local-set characterizations for backward solutions, for a given small ρ and for some ρ.

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.

theorem TauCeti.exists_pos_lyapunovPerronBound_mul_le (K α ε : NNReal) {r : ℝ} (hr0 : 0 < r) : ∃ ρ > 0, ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ρ ≤ r

A positive radius ρ satisfying K / (1 - 2 K (2 ε) / α) * ρ ≤ r. Nothing beyond 0 < r is assumed, so the coefficient is an arbitrary real number and may well be negative.

Under the smallness hypothesis 2 K (2 ε) < α that every caller below supplies, that coefficient is the Lyapunov--Perron bound on a solution in terms of its input parameter, and the inequality then says that an input parameter of norm at most ρ keeps the solution inside the ball of confinement of radius r. This is the bound on ρ that the local stable and unstable set descriptions below, and the homeomorphisms built from them in TauCeti/Analysis/ODE/LyapunovPerron/Embedding.lean, all assume.

noncomputable def ContinuousLinearMap.localStableGraphMap {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) < α) : X → X

The local stable graph map: the Lyapunov--Perron graph map of the nonlinearity N cut off outside the closed ball of radius r.

Under the bound on ρ in ContinuousLinearMap.setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image, its graph over range P ∩ closedBall 0 ρ is the local stable set of the equilibrium 0 of y' = A y + N y truncated by ‖P x‖ ≤ ρ.

Equations

• A.localStableGraphMap P N r hs hu hr hN hsmall = A.lyapunovPerronGraphMap P (N ∘ TauCeti.radialRetraction r) hs hu ⋯ ⋯ hsmall

@[simp]

theorem ContinuousLinearMap.apply_localStableGraphMap {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) < α) (hP : IsIdempotentElem P) (hAP : Commute A P) (ξ : X) : P (A.localStableGraphMap P N r hs hu hr hN hsmall ξ) = 0

The local stable graph map takes values in the kernel of P, so its graph over the range of P really is a graph.

@[simp]

theorem ContinuousLinearMap.localStableGraphMap_map {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) < α) (hP : IsIdempotentElem P) (ξ : X) : A.localStableGraphMap P N r hs hu hr hN hsmall (P ξ) = A.localStableGraphMap P N r hs hu hr hN hsmall ξ

The local stable graph map depends only on the P-component of its argument.

@[simp]

theorem ContinuousLinearMap.localStableGraphMap_zero {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) : A.localStableGraphMap P N r hs hu hr hN hsmall 0 = 0

If the nonlinearity fixes the equilibrium, so does the local stable graph map.

theorem ContinuousLinearMap.lipschitzWith_localStableGraphMap {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) < α) : LipschitzWith (2 * K * (ε * 2) / α * (K / (1 - 2 * K * (ε * 2) / α))) (A.localStableGraphMap P N r hs hu hr hN hsmall)

The local stable graph map is Lipschitz, with a constant that tends to 0 with the Lipschitz constant of the nonlinearity on the ball of confinement.

theorem ContinuousLinearMap.norm_localStableGraphMap_le {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) (ξ : X) : ‖A.localStableGraphMap P N r hs hu hr hN hsmall ξ‖ ≤ ↑(2 * K * (ε * 2) / α * (K / (1 - 2 * K * (ε * 2) / α))) * ‖ξ‖

If the nonlinearity fixes the equilibrium, the local stable set lies in a cone around the range of P whose opening tends to 0 with the Lipschitz constant of the nonlinearity.

theorem ContinuousLinearMap.hasFDerivAt_localStableGraphMap_zero {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) < α) (hr0 : 0 < r) (hN0 : N 0 = 0) (hN' : HasFDerivAt N 0 0) : HasFDerivAt (A.localStableGraphMap P N r hs hu hr hN hsmall) 0 0

The local stable graph map is flat at the equilibrium. If the nonlinear remainder fixes the equilibrium and has derivative zero there, then the local stable graph map also has derivative zero at the origin. When P is the commuting projection of an exponential dichotomy, ContinuousLinearMap.apply_localStableGraphMap then identifies this as tangency of the graph to range P.

theorem ContinuousLinearMap.contDiffAt_localStableGraphMap {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) {N' : X → X →L[ℝ] X} (hNd : ∀ x ∈ Metric.ball 0 r, HasFDerivAt N (N' x) x) (hN' : UniformContinuousOn N' (Metric.ball 0 r)) {ξ₀ : X} (hξ₀ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ‖ξ₀‖ < r) : ContDiffAt ℝ 1 (A.localStableGraphMap P N r hs hu hr hN hsmall) ξ₀

The local stable graph map is C¹. Suppose that N vanishes at the equilibrium and has derivative N' x at every point x of the open ball of radius r, with N' uniformly continuous there. Then the local stable graph map is continuously differentiable at every ξ₀ small enough that the uniform bound K / (1 - 2 K (2 ε) / α) ‖ξ₀‖ on the Lyapunov--Perron solution with parameter ξ₀ is less than r: the solution then stays strictly inside the ball, where the cutoff is invisible.

theorem ContinuousLinearMap.isIntegralCurveOn_comp_radialRetraction_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →L[ℝ] X} {N : X → X} {r : ℝ} {y : ℝ → X} (hmaps : Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) : IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Ici 0) ↔ IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + (N ∘ TauCeti.radialRetraction r) z) (Set.Ici 0)

Cutting off is invisible to a confined solution. A forward curve that never leaves the closed ball of radius r solves the original equation exactly when it solves the cut-off equation.

theorem ContinuousLinearMap.tendsto_of_isIntegralCurveOn_mapsTo_closedBall {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) {y : ℝ → X} (hy : IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Ici 0)) (hmaps : Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) : Filter.Tendsto y Filter.atTop (nhds 0)

A confined forward solution tends to the equilibrium. The ball of confinement is where the nonlinearity is small, so a solution that never leaves it is a Lyapunov--Perron solution of the cut-off equation, and those decay. This is what makes the set below a stable set.

theorem ContinuousLinearMap.setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image {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 | (∃ (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‖ ≤ ρ} = (fun (v : X) => v + A.localStableGraphMap P N r hs hu hr hN hsmall v) '' (Set.range ⇑P ∩ Metric.closedBall 0 ρ)

The local stable set at a hyperbolic equilibrium is a Lipschitz graph. The initial values of the solutions of y' = A y + N y on [0, ∞) that never leave the closed ball of radius r, restricted to those whose P-component has norm at most ρ, are exactly the points v + localStableGraphMap v with v in the range of P of norm at most ρ. Such solutions automatically tend to the equilibrium, by ContinuousLinearMap.tendsto_of_isIntegralCurveOn_mapsTo_closedBall.

The hypothesis on ρ is that the uniform bound K / (1 - 2 K (2 ε) / α) for Lyapunov--Perron solutions carries the ball of radius ρ into the ball of radius r; it is what makes the cutoff invisible to the solutions concerned.

theorem ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image {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, {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‖ ≤ ρ} = (fun (v : X) => v + A.localStableGraphMap P N r hs hu ⋯ hN hsmall v) '' (Set.range ⇑P ∩ Metric.closedBall 0 ρ)

The local stable-manifold theorem, Lipschitz form. Near a hyperbolic equilibrium the initial values of the forward solutions that stay in a fixed small ball, truncated by the condition ‖P x‖ ≤ ρ, form the graph of a Lipschitz map over a ball in the stable subspace range P.

noncomputable def ContinuousLinearMap.localUnstableGraphMap {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) < α) : X → X

The local unstable graph map, obtained by applying the local stable construction to the time-reversed equation. When P is idempotent it depends only on the component in the range of the complementary projection 1 - P, by ContinuousLinearMap.localUnstableGraphMap_sub_map; when P moreover commutes with A its values lie in the range of P, by ContinuousLinearMap.apply_localUnstableGraphMap.

Equations

• A.localUnstableGraphMap P N r hs hu hr hN hsmall = (-A).localStableGraphMap (ContinuousLinearMap.id ℝ X - P) (-N) r ⋯ ⋯ hr ⋯ hsmall

@[simp]

theorem ContinuousLinearMap.apply_localUnstableGraphMap {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) < α) (hP : IsIdempotentElem P) (hAP : Commute A P) (v : X) : P (A.localUnstableGraphMap P N r hs hu hr hN hsmall v) = A.localUnstableGraphMap P N r hs hu hr hN hsmall v

The local unstable graph map takes values in the kernel of the complementary projection, that is, P fixes them.

@[simp]

theorem ContinuousLinearMap.localUnstableGraphMap_sub_map {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) < α) (hP : IsIdempotentElem P) (v : X) : A.localUnstableGraphMap P N r hs hu hr hN hsmall (v - P v) = A.localUnstableGraphMap P N r hs hu hr hN hsmall v

The local unstable graph map depends only on the component in range (1 - P).

@[simp]

theorem ContinuousLinearMap.localUnstableGraphMap_zero {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) : A.localUnstableGraphMap P N r hs hu hr hN hsmall 0 = 0

If the nonlinearity fixes the equilibrium, so does the local unstable graph map.

theorem ContinuousLinearMap.hasFDerivAt_localUnstableGraphMap_zero {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) < α) (hr0 : 0 < r) (hN0 : N 0 = 0) (hN' : HasFDerivAt N 0 0) : HasFDerivAt (A.localUnstableGraphMap P N r hs hu hr hN hsmall) 0 0

The local unstable graph map is flat at the equilibrium. If the nonlinear remainder fixes the equilibrium and has derivative zero there, then the local unstable graph map also has derivative zero at the origin.

theorem ContinuousLinearMap.contDiffAt_localUnstableGraphMap {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) {N' : X → X →L[ℝ] X} (hNd : ∀ x ∈ Metric.ball 0 r, HasFDerivAt N (N' x) x) (hN' : UniformContinuousOn N' (Metric.ball 0 r)) {ξ₀ : X} (hξ₀ : ↑K / (1 - 2 * ↑K * (↑ε * 2) / ↑α) * ‖ξ₀‖ < r) : ContDiffAt ℝ 1 (A.localUnstableGraphMap P N r hs hu hr hN hsmall) ξ₀

The local unstable graph map is C¹ under the hypotheses of ContinuousLinearMap.contDiffAt_localStableGraphMap, by time reversal.

theorem ContinuousLinearMap.lipschitzWith_localUnstableGraphMap {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) < α) : LipschitzWith (2 * K * (ε * 2) / α * (K / (1 - 2 * K * (ε * 2) / α))) (A.localUnstableGraphMap P N r hs hu hr hN hsmall)

The local unstable graph map has the same Lipschitz bound as the stable graph map.

theorem ContinuousLinearMap.norm_localUnstableGraphMap_le {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) (v : X) : ‖A.localUnstableGraphMap P N r hs hu hr hN hsmall v‖ ≤ ↑(2 * K * (ε * 2) / α * (K / (1 - 2 * K * (ε * 2) / α))) * ‖v‖

If the nonlinearity fixes the equilibrium, the local unstable set lies in a cone around range (1 - P) whose opening tends to 0 with the Lipschitz constant of the nonlinearity. This is the unstable counterpart of ContinuousLinearMap.norm_localStableGraphMap_le.

theorem ContinuousLinearMap.tendsto_atBot_of_isIntegralCurveOn_mapsTo_closedBall {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) {y : ℝ → X} (hy : IsIntegralCurveOn y (fun (x : ℝ) (z : X) => A z + N z) (Set.Iic 0)) (hmaps : Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r)) : Filter.Tendsto y Filter.atBot (nhds 0)

A backward solution confined to the ball on which the nonlinearity is small tends to the equilibrium in backward time.

theorem ContinuousLinearMap.setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image {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 | (∃ (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‖ ≤ ρ} = (fun (v : X) => v + A.localUnstableGraphMap P N r hs hu hr hN hsmall v) '' (Set.range ⇑(ContinuousLinearMap.id ℝ X - P) ∩ Metric.closedBall 0 ρ)

The local unstable set at a hyperbolic equilibrium is a Lipschitz graph. The initial values of the solutions of y' = A y + N y on (-∞, 0] that never leave the closed ball of radius r, restricted to those whose 1 - P component has norm at most ρ, are exactly the points v + localUnstableGraphMap v with v in the range of 1 - P of norm at most ρ. Such solutions automatically tend to the equilibrium in backward time, by ContinuousLinearMap.tendsto_atBot_of_isIntegralCurveOn_mapsTo_closedBall.

The hypothesis on ρ is the one of ContinuousLinearMap.setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image, read for the time-reversed equation: time reversal changes neither the constants K, α nor the Lipschitz constant ε of the nonlinearity.

theorem ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image {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, {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‖ ≤ ρ} = (fun (v : X) => v + A.localUnstableGraphMap P N r hs hu ⋯ hN hsmall v) '' (Set.range ⇑(ContinuousLinearMap.id ℝ X - P) ∩ Metric.closedBall 0 ρ)

The local unstable-manifold theorem, Lipschitz form. Near a hyperbolic equilibrium the initial values of backward solutions confined to a fixed small ball, truncated by the norm of their 1 - P component, form a graph over a ball in range (1 - P).